let n be Element of NAT ; :: thesis: for a being Point of (TOP-REAL n)
for r being positive Real holds a in Ball (a,r)
let a be Point of (TOP-REAL n); :: thesis: for r being positive Real holds a in Ball (a,r)
let r be positive Real; :: thesis: a in Ball (a,r)
a - a = 0. (TOP-REAL n) by RLVECT_1:5;
then |.(a - a).| = 0 by EUCLID_2:39;
hence a in Ball (a,r) by TOPREAL9:7; :: thesis: verum