proposition: Lemma Not_Unbounded_countable (X : Ensemble Ord) : ~ Unbounded X -> Countable X.
proof: Proof. intros;eapply AX2;eauto. case (Not_Unbounded_bounded H);auto. intros x H0; exists x;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)