diff --git a/Analysis/MeasureTheory/Section_1_4_1.lean b/Analysis/MeasureTheory/Section_1_4_1.lean
index 59bee342..4a611c78 100644
--- a/Analysis/MeasureTheory/Section_1_4_1.lean
+++ b/Analysis/MeasureTheory/Section_1_4_1.lean
@@ -94,7 +94,24 @@ def IsNull.boolean_algebra (d:ℕ) : ConcreteBooleanAlgebra (EuclideanSpace' d)
     measurable := fun E => IsNull E ∨ IsNull Eᶜ
     empty_mem := by sorry
     compl_mem := by sorry
-    union_mem := by sorry
+    union_mem := fun E F hE hF => by
+      rcases hE with hE | hE <;> rcases hF with hF | hF
+      · refine Or.inl ?_
+        have hle : Lebesgue_outer_measure (E ∪ F) ≤
+            Lebesgue_outer_measure E + Lebesgue_outer_measure F := by
+          simpa [Fin.sum_univ_two] using
+            Lebesgue_outer_measure.finite_union_le (fun i : Fin 2 => if i = 0 then E else F)
+        simp [hE, hF] at hle
+        exact le_antisymm hle (Lebesgue_outer_measure.nonneg _)
+      · refine Or.inr (IsNull.subset hF ?_)
+        intro x hx
+        exact hx.2
+      · refine Or.inr (IsNull.subset hE ?_)
+        intro x hx
+        exact hx.1
+      · refine Or.inr (IsNull.subset hE ?_)
+        intro x hx
+        exact hx.1
   }
 
 def IsNull.lt_lebesgue_boolean_algebra (d:ℕ) :