proposition: Lemma Lemma5_7 : In (Cr alpha) (sup M).
proof: Proof. red; apply Cr_pos; auto. intros xi H; split. rewrite (A_full H). split. assert (continuous (phi xi) ordinal (Cr xi)). { apply Th_13_5_2. replace ordinal with (the_ordering_segment (Cr xi)). apply ord_ok. apply segment_unbounded. eapply ordering_function_seg with (Cr xi). exists (phi xi); apply ord_ok. assert (Unbounded (Cr xi)). now destruct (IHalpha H). rewrite (@ ordering_unbounded_unbounded (A_ xi) (Cr xi) (phi xi)) in H0. auto. apply ord_ok. destruct (IHalpha H); auto. } destruct H0. destruct H1. unfold phi in H2. rewrite <- H2. f_equal; apply Extensionality_Ensembles. split. intro x. destruct 1. destruct H3. subst; fold (phi xi x0); rewrite Lemma5_2; auto. intros x Hx; exists x; split; auto. fold (phi xi x); rewrite Lemma5_2; auto. split. auto. auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)