theorem fact_1_1 {α : Type u} [Preorder α] (h : ∀ (c : Set α), IsChain (fun (a b : α) => a ≤ b) c → BddAbove c) : ∃ (m : α), IsMax m

Fact 1.1 (Zorn's lemma): if every chain in a preorder has an upper bound, then there exists a maximal element.