proposition: Lemma range_id {A : Type} (U V : Ensemble A) : range id U V <-> Included U V.
proof: Proof. rewrite range_char_Im. rewrite Im_id. reflexivity. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)