proposition: Lemma sup_ok1 (X: Ensemble Ord)(HX : Countable X) : sup_spec X (sup X).
proof: Proof. unfold sup, the; apply iota_spec; now apply sup_spec_unicity. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)