proposition: Lemma no_ultra_zorn : forall a : E, ~ is_ultra_zorn a.
proof: Proof. uf not; ir. uh H; ee. set (c := max_uls a) in *. assert (is_ultra_linear_subset a c). uf c; ap max_uls_uls. am. set (x := ultra_bound a c) in *. assert (is_ultra_bound a c x). uf x. ap H0. uh H1; ee. uh H1; ee. am. ufk is_ultra_bound H2. ee. ap H3. uf c. apply ub_inc_max_uls with c. am. uhg; ee. am. tv. Qed.
imports: universe