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

Cl S = Cl (S /\ R)

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

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

A1: Cl S = Cl S1 by EQCL1;

A2: Cl (S1 /\ R1) = Cl (S /\ R) by EQCL1;

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

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

hence Cl S = Cl (S /\ R) by A1, A2, TOPS_1:46; :: thesis: verum

Cl S = Cl (S /\ R)

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

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

A1: Cl S = Cl S1 by EQCL1;

A2: Cl (S1 /\ R1) = Cl (S /\ R) by EQCL1;

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

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

hence Cl S = Cl (S /\ R) by A1, A2, TOPS_1:46; :: thesis: verum