proposition: Theorem ZornsLemma: exists x:T, maximal R x.
proof: Proof. pose proof (ZL' chains chains_ord chains_order chains_sup). apply NNPP. unfold maximal. pose proof chains_ord_exists. dintuition. assert (forall x:T, exists y:T, R x y /\ x <> y). - assert (forall x:T, ~ forall y:T, R x y -> x = y) by now apply not_ex_all_not. assert (forall x:T, exists y:T, ~ (R x y -> x = y)) as H3 by (intro; now apply not_all_ex_not). intro. destruct (H3 x) as [x0 H4]. exists x0. now apply imply_to_and. - assert (forall x:chains, exists y:chains, chains_ord x y /\ x <> y /\ forall z:chains, chains_ord x z -> chains_ord z y -> z = x \/ z = y) by intuition. apply choice in H3. destruct H3 as [f]. apply H. intro. exists (f x). apply H3. Qed.
imports: Classical ClassicalChoice Relation_Definitions Relation_Definitions_Implicit Ensembles EnsemblesImplicit ProofIrrelevance InverseImage EnsemblesSpec Quotients EnsemblesSpec