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