let X be RealNormSpace; :: thesis: for A, B being Subset of X st A c= B holds

Cl A c= Cl B

let A, B be Subset of X; :: thesis: ( A c= B implies Cl A c= Cl B )

assume A1: A c= B ; :: thesis: Cl A c= Cl B

reconsider A1 = A, B1 = B as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

A2: Cl A1 = Cl A by EQCL1;

Cl B1 = Cl B by EQCL1;

hence Cl A c= Cl B by A1, A2, PRE_TOPC:19; :: thesis: verum

Cl A c= Cl B

let A, B be Subset of X; :: thesis: ( A c= B implies Cl A c= Cl B )

assume A1: A c= B ; :: thesis: Cl A c= Cl B

reconsider A1 = A, B1 = B as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

A2: Cl A1 = Cl A by EQCL1;

Cl B1 = Cl B by EQCL1;

hence Cl A c= Cl B by A1, A2, PRE_TOPC:19; :: thesis: verum