proposition: Lemma sup_members_not_succ (alpha beta : Ord) : alpha = sup (members alpha) -> alpha <> succ beta.
proof: Proof. intros e e1; generalize (sup_of_leq beta). intro H; assert (sup (members alpha) = beta). { unfold members;rewrite H; apply sup_eq_intro. - apply AX2; exists alpha; auto. - apply AX2; exists (succ beta); intros y Hy; eauto with schutte. - red; intros; red; red in H0; rewrite e1 in H0. apply lt_succ_le_2;auto. - unfold Included, In; intros x H1; rewrite e1. eapply le_lt_trans;eauto with schutte. } case (@lt_irrefl alpha); pattern alpha at 2;rewrite e1, e, H0; auto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)