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