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

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