proposition: Theorem segment_unbounded : forall A:Ensemble Ord, segment A -> Unbounded A -> A = ordinal.
proof: Proof. Proof with eauto with schutte. intros A H H0; red in H0; apply Extensionality_Ensembles; split. - intros; split. - intros x Hx; destruct (H0 x) as [x0 H1]... destruct H1; now apply H with x0. Qed.
imports: ZornsLemma(CountableTypes)