theorem Th10: :: DECOMP_1:10

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