proposition: Lemma inverse_image_empty: forall {X Y:Type} (f:X->Y), inverse_image f Empty_set = Empty_set.
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. - destruct H as [[]]. - destruct H. Qed.
imports: ZornsLemma(IndexedFamilies Powerset_facts)