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, Th91; :: thesis: verum