let X be RealNormSpace; :: thesis: for R, S being Subset of X st R is dense & R c= S holds

S is dense

let R, S be Subset of X; :: thesis: ( R is dense & R c= S implies S is dense )

reconsider R1 = R, S1 = S as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

assume ( R is dense & R c= S ) ; :: thesis: S is dense

then ( R1 is dense & R1 c= S1 ) by EQCL2;

then S1 is dense by TOPS_1:44;

hence S is dense by EQCL2; :: thesis: verum

S is dense

let R, S be Subset of X; :: thesis: ( R is dense & R c= S implies S is dense )

reconsider R1 = R, S1 = S as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

assume ( R is dense & R c= S ) ; :: thesis: S is dense

then ( R1 is dense & R1 c= S1 ) by EQCL2;

then S1 is dense by TOPS_1:44;

hence S is dense by EQCL2; :: thesis: verum