proposition: Remark R6 : forall khi, In U khi -> khi <= alpha_ .
proof: Proof. Proof with eauto with schutte. intros khi H; case (R5 H). - left. + case (Ordering_bijection f_ord). intros H1 H2 H3; apply H3. * apply U_inc_A;auto. * apply alpha_A. * case H0;auto. - right; case f_ord; intros _ H1 H2 H3. tricho khi alpha_ H7; auto. + subst khi; case (@lt_irrefl _ H0). + case (@lt_irrefl (f alpha_));auto. apply lt_trans with (f khi); auto. * apply H3; auto. apply alpha_A; auto. Qed.
imports: ZornsLemma(CountableTypes)