proposition: Lemma is_limit_sup_members (alpha : Ord) : is_limit alpha -> alpha = |_| (members alpha).
proof: Proof. intros; case (@le_sup_members alpha);auto with schutte. intro H0; generalize (@sup_members_succ alpha). intros H1 ; destruct (not_is_limit_succ (alpha:=alpha));auto with schutte. exists (|_|members alpha); auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)