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