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