proposition: Lemma SpaceAdjunction_equivalence: equivalence SpaceAdjunction.
proof: Proof. split; red; intros; unfold SpaceAdjunction in *. - now left. - destruct H, H0; subst; now left + right. - destruct H, H; now left + right. Qed.
imports: ZornsLemma(InverseImage Powerset_facts Quotients) Topology(TopologicalSpaces)