proposition: Lemma countable_segment_proper : forall A : Ensemble Ord, segment A -> Countable A -> proper_segment A.
proof: Proof. intros A H H0; split;[auto|idtac]. intro H1; generalize (Extensionality_Ensembles _ _ H1). intros; subst A ; now case Non_denum. Qed.
imports: ZornsLemma(CountableTypes)