proposition: Lemma zorn : forall a : E, axioms a -> (forall b : E, is_linear_subset a b -> ex (fun x : E => is_upper_bound a b x)) -> ex (fun z : E => is_maximal a (U a) z).
proof: Proof. ir. ap excluded_middle. uf not; ir. apply no_ultra_zorn with a. uhg; dj. am. cp (H0 b H3). apply by_cases with (ex (fun y : E => is_ultra_bound a b y)). ir. cp (choose_pr H5). am. ir. assert False. ap H1. nin H4. sh x. uhg; dj. am. uf sub; ir; am. uh H4; ee. am. assert (is_upper_bound a b y). uhg; ee. am. uh H3; ee. am. am. ir. uh H4; ee. uh H; ee. apply H18 with x. ap H14; am. am. ap excluded_middle; uf not; ir. assert (is_top_element a b x). uhg; ee. am. ap excluded_middle. uf not; ir. ap H5. sh x. uhg; ee. am. am. assert (is_top_element a b y). uhg; ee. am. ap excluded_middle. uf not; ir. ap H5. sh y. uhg; ee. am. am. cp (top_element_unique H13 H14). ap H12; am. elim H6. Qed.
imports: universe