:: deftheorem defines PSO DECOMP_1:def 15 :
for T being TopSpace holds PSO T = { B where B is Subset of T : B is pre-semi-open } ;