:: deftheorem defines open_condensed TOPS_1:def 8 :
for GX being TopStruct
for R being Subset of GX holds
( R is open_condensed iff R = Int (Cl R) );