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

let V be Subset of X; :: 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 ) )
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 () st St is convergent & rng St c= Vt holds
Lim St c= Vt
let St be sequence of (); :: 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 ;
then lim S in V by ;
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 () ;
A8: St is convergent by ;
then Lim St c= Vt by ;
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