proposition: Theorem AP_o_segment : the_ordering_segment AP = ordinal.
proof: Proof. intros;apply segment_unbounded. eapply SA2. eapply ord_ok;eauto. generalize (ordering_unbounded_unbounded (A:=the_ordering_segment AP) (B:=AP) (f:=phi0)); intro H. generalize (H (ord_ok AP)); intro H0; rewrite <- H0. now apply AP_unbounded. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)