theorem Th15: :: DECOMP_1:15

for T being TopSpace holds (PSO T) /\ (D(p,ps) T) = PO T