let n be Element of NAT ; :: thesis: for r being Real
for A being Subset of (COMPLEX n) st 0 < r holds
A c= Ball (A,r)
let r be Real; :: thesis: for A being Subset of (COMPLEX n) st 0 < r holds
A c= Ball (A,r)
let A be Subset of (COMPLEX n); :: thesis: ( 0 < r implies A c= Ball (A,r) )
assume A1: r > 0 ; :: thesis: A c= Ball (A,r)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Ball (A,r) )
assume x in A ; :: thesis: x in Ball (A,r)
hence x in Ball (A,r) by A1, Th137; :: thesis: verum