let n be Nat; for r being Real
for z being Element of COMPLEX n
for A being Subset of (COMPLEX n) holds
( z in Ball (A,r) iff dist (z,A) < r )
let r be Real; for z being Element of COMPLEX n
for A being Subset of (COMPLEX n) holds
( z in Ball (A,r) iff dist (z,A) < r )
let z be Element of COMPLEX n; for A being Subset of (COMPLEX n) holds
( z in Ball (A,r) iff dist (z,A) < r )
let A be Subset of (COMPLEX n); ( z in Ball (A,r) iff dist (z,A) < r )
( z in { z2 where z2 is Element of COMPLEX n : dist (z2,A) < r } iff ex z1 being Element of COMPLEX n st
( z = z1 & dist (z1,A) < r ) )
;
hence
( z in Ball (A,r) iff dist (z,A) < r )
; verum