:: deftheorem defines pre-semi-open DECOMP_1:def 4 :
for T being TopStruct
for IT being Subset of T holds
( IT is pre-semi-open iff IT c= Cl (Int (Cl IT)) );