proposition: Lemma sup_exists : forall X, Countable X -> ex (sup_spec X).
proof: Proof. intros X H; case (AX3 H); auto. intros x H'x; assert (H''x : forall y : Ord, X y -> y=x \/ lt y x) by intuition. generalize (@well_order Ord lt AX1 (fun z => (forall y, X y -> y = z \/ y < z)) x ). intros H1; destruct H1 as [ x0 H0]. { red; auto. } exists x0; unfold least_member in H0; repeat split. - case H0; intros; intuition. red in H1; red; intros; auto. - intros y H1 H2; decompose [and] H0. red in H2; destruct (H4 y); auto. intros y0 H5; specialize (H2 y0); apply H2; auto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)