let X be RealNormSpace; :: thesis: for V being Subset of X

for Vt being Subset of (TopSpaceNorm X) st V = Vt holds

( V is open iff Vt is open )

let V be Subset of X; :: thesis: for Vt being Subset of (TopSpaceNorm X) st V = Vt holds

( V is open iff Vt is open )

let Vt be Subset of (TopSpaceNorm X); :: thesis: ( V = Vt implies ( V is open iff Vt is open ) )

A1: ( V is open iff V ` is closed ) by NFCONT_1:def 4;

assume V = Vt ; :: thesis: ( V is open iff Vt is open )

then ( V is open iff Vt ` is closed ) by A1, Th15;

hence ( V is open iff Vt is open ) by TOPS_1:4; :: thesis: verum

for Vt being Subset of (TopSpaceNorm X) st V = Vt holds

( V is open iff Vt is open )

let V be Subset of X; :: thesis: for Vt being Subset of (TopSpaceNorm X) st V = Vt holds

( V is open iff Vt is open )

let Vt be Subset of (TopSpaceNorm X); :: thesis: ( V = Vt implies ( V is open iff Vt is open ) )

A1: ( V is open iff V ` is closed ) by NFCONT_1:def 4;

assume V = Vt ; :: thesis: ( V is open iff Vt is open )

then ( V is open iff Vt ` is closed ) by A1, Th15;

hence ( V is open iff Vt is open ) by TOPS_1:4; :: thesis: verum