proposition: Theorem classification (alpha : Ord) : alpha = zero \/ is_succ alpha \/ is_limit alpha.
proof: Proof. case (le_sup_members alpha). - intro H; symmetry in H; case (sup_members_disj H);auto with schutte. - right; left; exists (sup (members alpha)); apply sup_members_succ;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)