proposition: Lemma L3a : segment (image B g).
proof: Proof. intros gbeta alpha (beta,(H1,H2)) H3; subst gbeta. generalize (g_lemma H1);intro. case H; intros H2 H4 H5 H6. assert (exists beta0, In (proper_segment_of B beta) beta0 /\ _f beta alpha=beta0). { exists (_f beta alpha); split;auto. } case H0;intros beta0 (H9,H10); clear H0. assert (B5 : ordering_function (_f beta) (members alpha) (proper_segment_of B beta0)). { repeat split; auto with schutte. - red; red; intros. apply lt_trans with alpha0;eauto. - assert( B2 : fun_bijection (members (g beta)) (proper_segment_of B beta) (_f beta)) . { apply Ordering_bijection ; apply g_lemma; auto. } case B2;intros H77 H11 H12; generalize (H77 a). intros H13; clear H77; case H13. 2:auto. red; apply lt_trans with alpha; auto. - case (g_lemma H1); intros. replace beta0 with (_f beta alpha). apply OF_mono0; auto. red; red; apply lt_trans with alpha;auto. - case H9; auto. - destruct 1; case (g_lemma H1); intros. case (OF_onto0 b). split;auto. split;auto. apply lt_trans with beta0;auto. case H7;auto. case H9;auto. destruct 2; auto. intros a (Ha,Ha');exists a;split;auto. red; tricho a alpha X. + auto. + subst a; rewrite H10 in Ha'. subst b. case H7; intros H77 _. case (@lt_irrefl _ H77). + assert (beta0 < b) by (rewrite <- H10; rewrite <- Ha'; auto). case (@lt_irrefl beta0). apply lt_trans with b;auto. case H7;auto. - intros; case (g_lemma H1); intros. apply OF_mono0; auto. red; apply lt_trans with alpha;auto. red; red; apply lt_trans with alpha;auto. } generalize (g_lemma (beta:=beta0));intros. case H9;intros H7 H8. generalize (H0 H7). intros H12; generalize (ordering_function_unicity B5 H12). destruct 1; generalize (Extensionality_Ensembles _ _ H11). intros H14; generalize (members_eq (alpha:=alpha)(beta:=g beta0) H14 ). exists beta0;split;auto. Qed.
imports: ZornsLemma(CountableTypes)