proposition: Lemma inverse_image_id {X : Type} (U : Ensemble X) : inverse_image (@id X) U = U.
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - apply H. - constructor. apply H. Qed.
imports: ZornsLemma(IndexedFamilies Powerset_facts)