:: deftheorem defines everywhere_dense TOPS_3:def 5 :
for X being TopStruct
for A being Subset of X holds
( A is everywhere_dense iff Cl (Int A) = the carrier of X );