:: deftheorem defines Ball SEQ_4:def 18 :
for n being Nat
for A being Subset of (COMPLEX n)
for r being Real holds Ball (A,r) = { z where z is Element of COMPLEX n : dist (z,A) < r } ;