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

let St be sequence of (TopSpaceNorm X); :: thesis: ( St is convergent & rng St c= Vt implies Lim St c= Vt )
assume A3: ( St is convergent & 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, A3, NFCONT_1:def 5;
then {(lim S)} c= V by ZFMISC_1:37;
hence Lim St c= Vt by A1, A3, Th14; :: thesis: verum

end;

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

end;

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

now

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

end;

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