proposition: Lemma Intersection_Im {X Y : Type} (f : X -> Y) (U V : Ensemble X) : Included (Im (Intersection U V) f) (Intersection (Im U f) (Im V f)).
proof: Proof. intros y Hy. destruct Hy as [x Hx y Hy]. subst. destruct Hx as [x HU HV]. split; exists x; auto. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(FunctionProperties)