proposition: Lemma SpaceAdjunction_equiv_class_Singleton (x : X): ~ In S x -> equiv_class SpaceAdjunction x = Singleton x.
proof: Proof. intros. extensionality_ensembles. - destruct H0; now subst. - auto with topology. Qed.
imports: ZornsLemma(InverseImage Powerset_facts Quotients) Topology(TopologicalSpaces)