diff --git a/Analysis/MeasureTheory/Section_1_4_1.lean b/Analysis/MeasureTheory/Section_1_4_1.lean
index 59bee342..9118a1e6 100644
--- a/Analysis/MeasureTheory/Section_1_4_1.lean
+++ b/Analysis/MeasureTheory/Section_1_4_1.lean
@@ -72,8 +72,11 @@ def JordanMeasurable.boolean_algebra (d:ℕ) : ConcreteBooleanAlgebra (Euclidean
   }
 
 def JordanMeasurable.gt_elementary_boolean_algebra (d:ℕ) :
-  JordanMeasurable.boolean_algebra d ≥ EuclideanSpace'.elementary_boolean_algebra d :=
-  by sorry
+  JordanMeasurable.boolean_algebra d ≥ EuclideanSpace'.elementary_boolean_algebra d := by
+  intro E hE
+  rcases hE with h | h
+  · exact Or.inl h.jordanMeasurable
+  · exact Or.inr h.jordanMeasurable
 
 /-- Example 1.4.5 (Lebesgue algebra) -/
 def LebesgueMeasurable.boolean_algebra (d:ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d) :=