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