for X being RealNormSpace st ex D being Subset of the carrier of X st
( D is dense & D is countable ) holds
X is separable