let X be RealNormSpace; :: thesis: for V being Subset of X
for Vt being Subset of (TopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
let V be Subset of X; :: thesis: for Vt being Subset of (TopSpaceNorm X) st V = Vt holds
( V is closed iff Vt is closed )
let Vt be Subset of (TopSpaceNorm X); :: thesis: ( V = Vt implies ( V is closed iff Vt is closed ) )
assume A1: V = Vt ; :: thesis: ( V is closed iff Vt is closed )

hereby :: thesis: ( Vt is closed implies V is closed )

assume A2: V is closed ; :: thesis: Vt is closed

now :: thesis: for St being sequence of (TopSpaceNorm X) st St is convergent & rng St c= Vt holds
Lim St c= Vt

let St be sequence of (TopSpaceNorm X); :: thesis: ( St is convergent & rng St c= Vt implies Lim St c= Vt )
assume that
A3: St is convergent and
A4: rng St c= Vt ; :: thesis: Lim St c= Vt
reconsider S = St as sequence of X ;
S is convergent by A3, Th13;
then lim S in V by A1, A2, A4, NFCONT_1:def 3;
then {(lim S)} c= V by ZFMISC_1:31;
hence Lim St c= Vt by A1, A3, Th14; :: thesis: verum

end;

hence Vt is closed by FRECHET:def 7; :: thesis: verum

end;

assume A5: Vt is closed ; :: thesis: V is closed

now :: thesis: for S being sequence of X st rng S c= V & S is convergent holds
lim S in V

let S be sequence of X; :: thesis: ( rng S c= V & S is convergent implies lim S in V )
assume that
A6: rng S c= V and
A7: S is convergent ; :: thesis: lim S in V
reconsider St = S as sequence of (TopSpaceNorm X) ;
A8: St is convergent by A7, Th13;
then Lim St c= Vt by A1, A5, A6, FRECHET:def 7;
then {(lim S)} c= V by A1, A8, Th14;
hence lim S in V by ZFMISC_1:31; :: thesis: verum

end;

hence V is closed by NFCONT_1:def 3; :: thesis: verum