proposition: Lemma sup_spec_unicity (X:Ensemble Ord) (HX : Countable X) : exists! u, sup_spec X u.
proof: Proof. destruct (sup_exists HX). exists x;split;auto. intros; apply sup_unicity with X;split;auto. 1, 2, 4 : split. - destruct H; tauto. - destruct H0; tauto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)