let n be Element of NAT ; :: thesis: for r being positive real number
for a being Point of holds a in Ball a,r
let r be positive real number ; :: thesis: for a being Point of holds a in Ball a,r
let a be Point of ; :: thesis: a in Ball a,r
|.(a - a).| = 0 by TOPRNS_1:29;
hence a in Ball a,r by TOPREAL9:7; :: thesis: verum