proposition: Lemma lt_sup_exists_lt (X : Ensemble Ord) : Countable X -> forall y, y < sup X -> exists x, In X x /\ y < x.
proof: Proof. intros H y H0; case (not_all_not_ex _ (fun x => X x /\ y < x)). - red;intro H1; assert (forall n, X n -> n <= y). { intros n H4; apply NNPP. intro H5. assert (y < n). { case (@trichotomy n y). - intro H6; case H5;auto with schutte. - destruct 1. + case H5;auto with schutte. + auto. } case (H1 n); split;auto with schutte. } assert (sup X <= y). { apply sup_least_upper_bound; auto. } case (@Lt_irreflexive Ord lt AX1 y). eapply Lt_Le_trans;eauto with schutte. - intros x Hx; exists x;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)