proposition: Lemma SpaceAdjunction_equiv_class_cases (x : X): ~ In S x /\ equiv_class SpaceAdjunction x = Singleton x \/ In S x.
proof: Proof. destruct (classic (In S x)). - now right. - left. split; trivial. now rewrite SpaceAdjunction_equiv_class_Singleton. Qed.
imports: ZornsLemma(InverseImage Powerset_facts Quotients) Topology(TopologicalSpaces)