proposition: Lemma Im_monotonous {X Y : Type} (f : X -> Y) (U V : Ensemble X) : Included U V -> Included (Im U f) (Im V f).
proof: Proof. intros. red. intros. inversion H0; subst; clear H0. apply H in H1. exists x0; auto. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(FunctionProperties)