proposition: Lemma inverse_image_image_surjective {X Y : Type} (f : X -> Y) (T : Ensemble Y) : surjective f -> Im (inverse_image f T) f = T.
proof: Proof. intros. apply inverse_image_image_surjective_locally. intros. apply H. Qed.
imports: ZornsLemma(IndexedFamilies Powerset_facts)