proposition: Lemma sup_of_leq (alpha : Ord) : alpha = |_| (fun x : Ord => x <= alpha).
proof: Proof. assert (DD :Countable (fun x : Ord => x <= alpha)). { apply AX2. - exists (succ alpha); destruct 1; apply le_lt_trans with alpha;auto with schutte. } apply le_antisym. - apply sup_upper_bound; auto with schutte. - apply sup_least_upper_bound;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)