theorem Th12: :: RUSUB_7:12

for S being RealUnitarySpace
for X being Subset of S holds
( X is closed Subset of (TopSpaceNorm (RUSp2RNSp S)) iff for s1 being sequence of S st rng s1 c= X & s1 is convergent holds
lim s1 in X )