proposition: Lemma sup_members_succ (alpha : Ord) : sup (members alpha) < alpha -> alpha = succ (|_| (members alpha)).
proof: Proof. intros H;pose (A := sup (members alpha)). fold A; generalize (@lt_succ_le A alpha). intros H0. case (le_eq_or_lt (H0 H)). - symmetry;auto. - intro H3; assert (succ A <= A). { unfold A;apply sup_upper_bound. - apply AX2; exists alpha;unfold members; auto. - assumption. } destruct (@lt_irrefl A); apply lt_le_trans with (succ A); auto. + eapply lt_succ;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)