let n be Element of NAT ; :: thesis: for r being Real
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st 0 < r & x in A holds
x in Ball A,r
let r be Real; :: thesis: for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st 0 < r & x in A holds
x in Ball A,r
let x be Element of COMPLEX n; :: thesis: for A being Subset of (COMPLEX n) st 0 < r & x in A holds
x in Ball A,r
let A be Subset of (COMPLEX n); :: thesis: ( 0 < r & x in A implies x in Ball A,r )
assume that
A1: 0 < r and
A2: x in A ; :: thesis: x in Ball A,r
dist x,A = 0 by A2, Th87;
hence x in Ball A,r by A1; :: thesis: verum