proposition: Lemma Not_Unbounded_bounded (X: Ensemble Ord): ~ Unbounded X -> exists beta : Ord, forall x, In X x -> x < beta.
proof: Proof. intros H; apply NNPP; intro H0. assert (forall beta, exists x, In X x /\ beta <= x). { intros beta; change (exists x:Ord, (fun y => In X y /\ beta <= y) x). apply not_all_not_ex. intro H1; case H0; exists beta; auto. - intros x H2; tricho x beta H5;auto with schutte. + case (H1 x). split;auto with schutte. + case (H1 x);split;auto with schutte. } clear H0; case H; intro x. destruct (H1 (succ x)) as [y [H2 H3]]. exists y;split;auto with schutte. apply lt_le_trans with (succ x); auto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)