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

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

( V is closed iff Vt is closed )

let V be Subset of 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 ) )

reconsider VVt = Vt as Subset of (TopSpaceNorm X) by Def4;

assume A1: V = Vt ; :: thesis: ( V is closed iff Vt is closed )

( Vt is closed iff VVt is closed ) by Th21;

hence ( V is closed iff Vt is closed ) by A1, Th15; :: thesis: verum

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

( V is closed iff Vt is closed )

let V be Subset of 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 ) )

reconsider VVt = Vt as Subset of (TopSpaceNorm X) by Def4;

assume A1: V = Vt ; :: thesis: ( V is closed iff Vt is closed )

( Vt is closed iff VVt is closed ) by Th21;

hence ( V is closed iff Vt is closed ) by A1, Th15; :: thesis: verum