proposition: Lemma g_def1 : exists g_beta: Ord, ordinal g_beta /\ _A = members g_beta.
proof: Proof. generalize (proper_members Proper_A); intros (a,Ha);exists a;split. - now destruct Ha. - eapply Extensionality_Ensembles; tauto. Qed.
imports: ZornsLemma(CountableTypes)