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

( 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