proposition: Lemma lt_sup_exists_leq (X: Ensemble Ord) : Countable X -> forall y, y < sup X -> exists x, In X x /\ y <= x.
proof: Proof. intros; case (not_all_not_ex _ (fun x => X x /\ y <= x)). - intro H3; unfold Included,In in H0. assert (forall n, X n -> n < y). { intros n H4; apply NNPP; intro H5. assert (y < n). { case (@trichotomy n y); auto. - intro; case H5;auto. - destruct 1. + subst n ; case (H3 y). auto with schutte. + auto. } case (H3 n). split;auto with schutte. } case ( @lt_irrefl y). eapply lt_le_trans with (|_|X);eauto. apply sup_least_upper_bound;auto with schutte. - intros x Hx; exists x;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)