let X be RealNormSpace; :: thesis: for V being Subset of
for Vt being Subset of st V = Vt holds
( V is closed iff Vt is closed )
let V be Subset of ; :: thesis: for Vt being Subset of st V = Vt holds
( V is closed iff Vt is closed )
let Vt be Subset of ; :: thesis: ( V = Vt implies ( V is closed iff Vt is closed ) )
reconsider VVt = Vt as Subset of 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