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