theorem Th16: :: DECOMP_1:16

for T being TopSpace holds (PSO T) /\ (D(alpha,p) T) = SO T