for T being TopSpace holds (PO T) /\ (D(c,p) T) = the topology of T