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