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 closed iff Vt is closed )
let V be Subset of (TopSpaceNorm X); :: thesis: for Vt being Subset of (LinearTopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
let Vt be Subset of (LinearTopSpaceNorm X); :: thesis: ( V = Vt implies ( V is closed iff Vt is closed ) )
assume V = Vt ; :: thesis: ( V is closed iff Vt is closed )
then A1: Vt ` = V ` by Def4;
( Vt is closed iff V ` is open ) by A1, Th20;
hence ( V is closed iff Vt is closed ) ; :: thesis: verum