proposition: Lemma le_cardinal_ens_wf {X : Type} (F : Family X) : Inhabited F -> exists U, least_cardinal_subset F U.
proof: Proof. Admitted. Corollary least_cardinal_ext_exists {X : Type} (F : Family X) : Inhabited F -> exists U : Ensemble X, least_cardinal_ext F U. Proof. intros HF. destruct (le_cardinal_ens_wf F HF) as [U HU]. exists U. apply least_cardinal_ext_subset. assumption. Qed.
imports: Coq(ClassicalChoice Description Lia PeanoNat Program.Subset) ZornsLemma(Cardinals CountableTypes CSB DecidableDec Families Finite_sets FiniteTypes FunctionProperties FunctionPropertiesEns InverseImage Powerset_facts Proj1SigInjective ReverseMath.AddSubtract) Coq(RelationClasses)