proposition: Lemma SpaceAdjunction_equiv_class_S (x : X): In S x -> equiv_class SpaceAdjunction x = S.
proof: Proof. intro. extensionality_ensembles. - destruct H0, H0; now subst. - constructor. now right. Qed.
imports: ZornsLemma(InverseImage Powerset_facts Quotients) Topology(TopologicalSpaces)