proposition: Lemma inverse_image_Im_adjoint {A B : Type} (f : A -> B) (U : Ensemble A) (V : Ensemble B) : Included (Im U f) V <-> Included U (inverse_image f V).
proof: Proof. unfold Included, inverse_image. firstorder. - apply H, Im_def, H0. - inversion H0; subst; clear H0. specialize (H x0 H1). destruct H. assumption. Qed.
imports: ZornsLemma(IndexedFamilies Powerset_facts)