let n be Nat; :: thesis: for r being positive Real
for a being Point of (TOP-REAL n) holds a in Ball (a,r)
let r be positive Real; :: 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:28;
hence a in Ball (a,r) by TOPREAL9:7; :: thesis: verum