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