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

( A is open iff Cl (([#] X) \ A) = ([#] X) \ A )

let A be Subset of X; :: thesis: ( A is open iff Cl (([#] X) \ A) = ([#] X) \ A )

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

A1: [#] X = [#] (LinearTopSpaceNorm X) by NORMSP_2:def 4;

A2: Cl (([#] (LinearTopSpaceNorm X)) \ A1) = Cl (([#] X) \ A) by A1, EQCL1;

( A1 is open iff A is open ) by NORMSP_2:33;

hence ( A is open iff Cl (([#] X) \ A) = ([#] X) \ A ) by A1, A2, PRE_TOPC:23; :: thesis: verum

( A is open iff Cl (([#] X) \ A) = ([#] X) \ A )

let A be Subset of X; :: thesis: ( A is open iff Cl (([#] X) \ A) = ([#] X) \ A )

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

A1: [#] X = [#] (LinearTopSpaceNorm X) by NORMSP_2:def 4;

A2: Cl (([#] (LinearTopSpaceNorm X)) \ A1) = Cl (([#] X) \ A) by A1, EQCL1;

( A1 is open iff A is open ) by NORMSP_2:33;

hence ( A is open iff Cl (([#] X) \ A) = ([#] X) \ A ) by A1, A2, PRE_TOPC:23; :: thesis: verum