:: deftheorem defines closed SEQ_4:def 15 :
for n being Nat
for A being Subset of (COMPLEX n) holds
( A is closed iff for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) holds
x in A );