proposition: Remark R : exists! z : Ord, least_member lt ordinal z.
proof: Proof. destruct inh_Ord as [a ]; apply least_member_ex_unique with a. - apply AX1. - split. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)