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

R /\ S is dense

let R, S be Subset of X; :: thesis: ( R is dense & S is dense & S is open implies R /\ S is dense )

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

assume ( R is dense & S is dense & S is open ) ; :: thesis: R /\ S is dense

then ( R1 is dense & S1 is dense & S1 is open ) by EQCL2, NORMSP_2:33;

then R1 /\ S1 is dense by TOPS_1:47;

hence R /\ S is dense by EQCL2; :: thesis: verum

R /\ S is dense

let R, S be Subset of X; :: thesis: ( R is dense & S is dense & S is open implies R /\ S is dense )

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

assume ( R is dense & S is dense & S is open ) ; :: thesis: R /\ S is dense

then ( R1 is dense & S1 is dense & S1 is open ) by EQCL2, NORMSP_2:33;

then R1 /\ S1 is dense by TOPS_1:47;

hence R /\ S is dense by EQCL2; :: thesis: verum