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