let m be Nat; :: thesis: for r being Real
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; :: 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: now :: thesis: for a, b being Point of (TOP-REAL m) st a in Ball (b,r) holds
- a in Ball ((- b),r)
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 A2: |.(a - b).| < r by 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 A2, TOPREAL9:7; :: thesis: verum
end;
( - (- p) = p & - (- q) = q ) ;
hence ( p in Ball (q,r) iff - p in Ball ((- q),r) ) by A1; :: thesis: verum