proposition: Lemma SpaceAdjunction_quotient_projection_injective (x y : X): ~ In S x -> quotient_projection SpaceAdjunction x = quotient_projection SpaceAdjunction y -> x = y.
proof: Proof. intros. apply quotient_projection_minimally_collapses_R in H0; auto with topology. now destruct H0. Qed.
imports: ZornsLemma(InverseImage Powerset_facts Quotients) Topology(TopologicalSpaces)