∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder α] {s : Set α},
  s.Countable → (∀ (x : α), ∃ y ∈ s, x ≤ y) → DirectedOn (fun x1 x2 => x1 ≤ x2) s → ⨆ x ∈ s, μ (Set.Iic x) = μ Set.univ