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 12;

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:31 ;
then |.((- a) - (- b)).| = |.(a - b).| by EUCLID:71;
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