proposition: Theorem unbounded : forall alpha, exists beta, alpha < beta.
proof: Proof. intros alpha ; pose (X0 := fun z => z < alpha). assert (Countable X0). { apply AX2. unfold X0, Included, In; intuition. now exists alpha. } pose (X:= Add X0 alpha). assert (Countable X). { apply countable_union2. auto. apply countable_singleton. } case (AX3 H0); intros x Hx. assert (H1: X alpha). { unfold X; right; split. } specialize (Hx alpha H1); exists x;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)