let X be NormedLinearTopSpace; :: thesis: for RNS being RealNormSpace
for V being Subset of X
for W being Subset of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) & V = W holds
( V is closed iff W is closed )
let RNS be RealNormSpace; :: thesis: for V being Subset of X
for W being Subset of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) & V = W holds
( V is closed iff W is closed )
let V be Subset of X; :: thesis: for W being Subset of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) & V = W holds
( V is closed iff W is closed )
let V0 be Subset of RNS; :: thesis: ( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) & V = V0 implies ( V is closed iff V0 is closed ) )
assume A1: ( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) & V = V0 ) ; :: thesis: ( V is closed iff V0 is closed )

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

assume A2: V is closed ; :: thesis: V0 is closed
for s2 being sequence of RNS st rng s2 c= V0 & s2 is convergent holds
lim s2 in V0

proof

let s2 be sequence of RNS; :: thesis: ( rng s2 c= V0 & s2 is convergent implies lim s2 in V0 )
reconsider s1 = s2 as sequence of X by A1;
assume A3: ( rng s2 c= V0 & s2 is convergent ) ; :: thesis: lim s2 in V0
then A4: s1 is convergent by Th27, A1;
then lim s1 = lim s2 by Th26, A1;
hence lim s2 in V0 by A1, A2, Th28, A3, A4; :: thesis: verum

end;

hence V0 is closed ; :: thesis: verum

end;

assume A5: V0 is closed ; :: thesis: V is closed
for s2 being sequence of X st rng s2 c= V & s2 is convergent holds
lim s2 in V

proof

let s2 be sequence of X; :: thesis: ( rng s2 c= V & s2 is convergent implies lim s2 in V )
assume A6: ( rng s2 c= V & s2 is convergent ) ; :: thesis: lim s2 in V
reconsider s1 = s2 as sequence of RNS by A1;
A7: s1 is convergent by Th27, A1, A6;
lim s1 = lim s2 by Th26, A1, A6;
hence lim s2 in V by A1, A5, A6, A7; :: thesis: verum

end;

hence V is closed by Th28; :: thesis: verum