proposition: Lemma ordering_segments_of_B (beta : Ord) : In B beta -> exists! A : Ensemble Ord, ordering_segment A (proper_segment_of B beta).
proof: Proof. Proof with eauto with schutte. intros Hbeta; pattern beta; apply transfinite_induction. - intros a H0; apply L3_u. + intros beta0 H1; rewrite <- (proper_of_proper (B:=B) (beta:=a) (beta':=beta0))... apply H0... * destruct H1 ; tauto. * destruct H1; tauto. Qed.
imports: ZornsLemma(CountableTypes)