English
If S is a collection of sets closed under inclusion and every chain has an upper bound contained in supersets, there exists a minimal element in S.
Русский
Если S — множество множеств, замкнутое по включению, и каждая цепь имеет верхнюю грань, содержащуюся в надмножестве, существует минимальная величина в S.
LaTeX
$$$$\forall {\alpha} (S:\Set(\Set \alpha)), (H : \forall c \\subseteq S, IsChain (\\subseteq) c \\to \exists lb \in S, \forall s \\in c, lb \\subseteq s) \\to \exists m, \text{Minimal}(\\in S) m.$$$$
Lean4
theorem zorn_superset (S : Set (Set α)) (h : ∀ c ⊆ S, IsChain (· ⊆ ·) c → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s) :
∃ m, Minimal (· ∈ S) m :=
(@zorn_le₀ (Set α)ᵒᵈ _ S) fun c cS hc => h c cS hc.symm
