proposition: Remark A_full : forall xi, xi < alpha -> A_ xi = ordinal.
proof: Proof. unfold A_; intros. replace (the_ordering_segment (Cr xi)) with ordinal . split. symmetry; apply segment_unbounded. eapply ordering_function_seg with (Cr xi). unfold the_ordering_segment, the. apply iota_ind. apply ordering_segment_ex_unique. destruct 1; auto. rewrite <- (@ ordering_unbounded_unbounded (A_ xi) (Cr xi) (phi xi)). destruct (IHalpha H);auto. apply ord_ok. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)