proposition: Lemma inverse_image_complement: forall {X Y:Type} (f:X->Y) (T:Ensemble Y), inverse_image f (Complement T) = Complement (inverse_image f T).
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. - red; intro. destruct H. destruct H0. contradiction H. - constructor. intro. contradiction H. constructor; trivial. Qed.
imports: ZornsLemma(IndexedFamilies Powerset_facts)