proposition: Lemma SpaceAdjunction_equiv_class_Singleton_eq (x y : X): equiv_class SpaceAdjunction x = Singleton y -> S <> Singleton y -> x = y.
proof: Proof. intros. destruct (SpaceAdjunction_equiv_class_cases x) as [[? ?] | ?]. - rewrite H in H2. now apply Singleton_injective. - now rewrite SpaceAdjunction_equiv_class_S in H. Qed.
imports: ZornsLemma(InverseImage Powerset_facts Quotients) Topology(TopologicalSpaces)