proposition: Lemma le_cardinal_ens_Included {X : Type} (U V : Ensemble X) : Included U V -> le_cardinal_ens U V.
proof: Proof. right. exists id. firstorder. 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)