proposition: Lemma le_sup_members (alpha : Ord) : |_| (members alpha) <= alpha.
proof: Proof. intros; apply sup_least_upper_bound; auto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)