:: deftheorem defines Ball SEQ_4:def 16 :
for n being Nat
for x being Element of COMPLEX n
for r being Real holds Ball (x,r) = { z where z is Element of COMPLEX n : |.(z - x).| < r } ;