let n be 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, Th115;
hence x in Ball (A,r) by A1; :: thesis: verum