let X be RealNormSpace; :: thesis: ( ex D being Subset of the carrier of X st
( D is dense & D is countable ) implies X is separable )
set Y = LinearTopSpaceNorm X;
given D0 being Subset of the carrier of X such that A1: ( D0 is dense & D0 is countable ) ; :: thesis: X is separable
reconsider D = D0 as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
D is dense by A1, NORMSP_3:15;
then A2: density (LinearTopSpaceNorm X) c= card D by TOPGEN_1:def 12;
card D c= omega by A1;
then density (LinearTopSpaceNorm X) c= omega by A2;
hence X is separable by TOPGEN_1:def 13; :: thesis: verum