theorem Th17: :: DECOMP_1:17

for T being TopSpace holds (PSO T) /\ (D(sp,ps) T) = SPO T