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