:: deftheorem defines closed CFDIFF_1:def 10 :
for X being Subset of COMPLEX holds
( X is closed iff for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent holds
lim s1 in X );