let n be Nat; :: thesis: for r being Real
for x being Element of COMPLEX n st 0 < r holds
x in Ball (x,r)
let r be Real; :: thesis: for x being Element of COMPLEX n st 0 < r holds
x in Ball (x,r)
let x be Element of COMPLEX n; :: thesis: ( 0 < r implies x in Ball (x,r) )
assume A1: 0 < r ; :: thesis: x in Ball (x,r)
|.(x - x).| = 0 by Th101;
hence x in Ball (x,r) by A1; :: thesis: verum