proposition: Lemma sup_eq_intro (X Y : Ensemble Ord): Countable X -> Countable Y -> Included X Y -> Included Y X -> |_| X = |_| Y.
proof: Proof. unfold Included, In; intros; apply le_antisym; apply sup_mono;auto with schutte; intro x;exists x; unfold In;auto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)