let m be Nat; :: thesis: for r being real number
for p, q being Point of (TOP-REAL m) holds
( p in Ball q,r iff - p in Ball (- q),r )
let r be real number ; :: thesis: for p, q being Point of (TOP-REAL m) holds
( p in Ball q,r iff - p in Ball (- q),r )
let p, q be Point of (TOP-REAL m); :: thesis: ( p in Ball q,r iff - p in Ball (- q),r )
A1: m in NAT by ORDINAL1:def 13;

A2: now

let a, b be Point of (TOP-REAL m); :: thesis: ( a in Ball b,r implies - a in Ball (- b),r )
assume a in Ball b,r ; :: thesis: - a in Ball (- b),r
then A3: |.(a - b).| < r by A1, TOPREAL9:7;
(- a) - (- b) = (- a) + (- (- b))
.= - (a - b) by RLVECT_1:45 ;
then |.((- a) - (- b)).| = |.(a - b).| by EUCLID:75;
hence - a in Ball (- b),r by A1, A3, TOPREAL9:7; :: thesis: verum

end;

( - (- p) = p & - (- q) = q ) ;
hence ( p in Ball q,r iff - p in Ball (- q),r ) by A2; :: thesis: verum