proposition: Lemma Lemma5_03 : In (Cr alpha) gamma.
proof: Proof. red; apply Cr_pos; auto. intros xi Hxi; unfold P in IHalpha; split. - red; assert (Unbounded (Cr xi)) by (now destruct (IHalpha Hxi)). rewrite (@ ordering_unbounded_unbounded (A_ xi) (Cr xi) (phi xi)) in H. replace (the_ordering_segment (Cr xi)) with ordinal . + split. + symmetry; apply segment_unbounded. * eapply ordering_function_seg with (Cr xi). exists (phi xi); apply ord_ok; auto. * auto. + apply ord_ok. - apply Lemma5_02; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)