:: deftheorem defines dense NORMSP_3:def 2 :
for X being RealNormSpace
for A being Subset of X holds
( A is dense iff Cl A = [#] X );