theorem :: NORMSP_3:14

for X being RealNormSpace
for A being Subset of X holds
( A is dense iff for x being Point of X ex seq being sequence of X st
( rng seq c= A & seq is convergent & lim seq = x ) )