proposition: Lemma sup_upper_bound (X : Ensemble Ord) (alpha : Ord): Countable X -> In X alpha -> alpha <= |_| X.
proof: Proof. intros H H1; generalize (sup_ok1 H). intro H2; destruct H2 as [H2 [H3 H4]]. destruct (H3 alpha); auto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)