let X be RealNormSpace; :: thesis: for V being Subset of (TopSpaceNorm X)
for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )
let V be Subset of (TopSpaceNorm X); :: thesis: for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )
let Vt be Subset of (LinearTopSpaceNorm X); :: thesis: ( V = Vt implies ( V is open iff Vt is open ) )
( Vt is open iff Vt in the topology of (LinearTopSpaceNorm X) ) by PRE_TOPC:def 5;
then A1: ( Vt is open iff Vt in the topology of (TopSpaceNorm X) ) by Def4;
assume V = Vt ; :: thesis: ( V is open iff Vt is open )
hence ( V is open iff Vt is open ) by A1, PRE_TOPC:def 5; :: thesis: verum