English
If S is a family of sets and every chain in S under inclusion has an upper bound in S, then there exists a maximal element in S with respect to inclusion.
Русский
Если S — это семейство множеств и каждая цепь в S по включению имеет верхнюю грань внутри S, то существует максимальный элемент в S по включению.
LaTeX
$$$$\forall {\alpha} [\text{Type }\alpha], (S:\text{Set }(\text{Set }\alpha)) \\to (\\forall c \\subseteq S, IsChain (\\subseteq) c \\to \exists ub \in S, \forall s \\in c, s \\subseteq ub) \\to \exists m \\in S, \text{Maximal}(\\in S) m.$$$$
Lean4
theorem zorn_subset (S : Set (Set α)) (h : ∀ c ⊆ S, IsChain (· ⊆ ·) c → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub) :
∃ m, Maximal (· ∈ S) m :=
zorn_le₀ S h
