proposition: Lemma sup_least_upper_bound (X : Ensemble Ord) (alpha : Ord) : Countable X -> (forall y, In X y -> y <= alpha) -> sup X <= alpha.
proof: Proof. intros H H0; specialize (sup_ok1 H) as H1. destruct H1 as [H1 [H2 H3]]. destruct (H3 alpha); auto with schutte. red; intros; apply H0; auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)