let n be Element of 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 Th72;
hence x in Ball x,r by A1; :: thesis: verum