{α : Type u_7} →
  (MeasurableSet' : Set α → Prop) →
    MeasurableSet' ∅ →
      (∀ (s : Set α), MeasurableSet' s → MeasurableSet' sᶜ) →
        (∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet' (f i)) → MeasurableSet' (⋃ i, f i)) → MeasurableSpace α