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