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