let X be RealNormSpace; :: thesis: for A, B being Subset of X holds Cl (A /\ B) c= (Cl A) /\ (Cl B)
let A, B be Subset of X; :: thesis: Cl (A /\ B) c= (Cl A) /\ (Cl B)
reconsider A1 = A, B1 = B as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
A1: Cl A1 = Cl A by EQCL1;
A2: Cl B1 = Cl B by EQCL1;
Cl (A1 /\ B1) = Cl (A /\ B) by EQCL1;
hence Cl (A /\ B) c= (Cl A) /\ (Cl B) by A1, A2, PRE_TOPC:21; :: thesis: verum