let X be RealNormSpace; :: thesis: for A being Subset of X holds

( A is closed iff Cl A = A )

let A be Subset of X; :: thesis: ( A is closed iff Cl A = A )

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

A1: Cl A1 = Cl A by EQCL1;

( A1 is closed iff A is closed ) by NORMSP_2:32;

hence ( A is closed iff Cl A = A ) by A1, PRE_TOPC:22; :: thesis: verum

( A is closed iff Cl A = A )

let A be Subset of X; :: thesis: ( A is closed iff Cl A = A )

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

A1: Cl A1 = Cl A by EQCL1;

( A1 is closed iff A is closed ) by NORMSP_2:32;

hence ( A is closed iff Cl A = A ) by A1, PRE_TOPC:22; :: thesis: verum