theorem :: NORMSP_3:21

for X being RealNormSpace holds
( X is separable iff ex seq being sequence of X st rng seq is dense )