proposition: Lemma image_inverse_image_included {X Y} (f : X -> Y) (U : Ensemble Y) : Included (Im (inverse_image f U) f) U.
proof: Proof. rewrite inverse_image_Im_adjoint. reflexivity. Qed.
imports: ZornsLemma(IndexedFamilies Powerset_facts)