proposition: Lemma not_inhabited_empty {X : Type} (U : Ensemble X) : ~ Inhabited U -> U = Empty_set.
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. - contradict H. exists x. assumption. - destruct H0. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)