:: deftheorem defines condensed TOPS_1:def 6 :
for GX being TopStruct
for R being Subset of GX holds
( R is condensed iff ( Int (Cl R) c= R & R c= Cl (Int R) ) );