theorem Th28: :: C0SP3:28
for X being NormedLinearTopSpace
for V being Subset of X holds
( V is closed iff for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V )