theorem Th26: :: NORMSP_4:21

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