:: deftheorem defines ^alpha DECOMP_1:def 11 :
for T being TopSpace holds T ^alpha = { B where B is Subset of T : B is alpha-set of T } ;