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