let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: verum