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