proposition: Lemma Unbounded_not_countable (X: Ensemble Ord) : Unbounded X -> not (Countable X).
proof: Proof. intros H H1; case (AX3 H1); intros x Hx. destruct (H x) as [x0 [H0 H2]]. case (Lt_irreflexive (a:=x)); eapply (Lt_trans (WO:=AX1)); eauto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)