:: deftheorem defines closed NFCONT_1:def 3 :
for S being RealNormSpace
for X being Subset of S holds
( X is closed iff for s1 being sequence of S st rng s1 c= X & s1 is convergent holds
lim s1 in X );