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) )

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

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)

( - (- p) = p & - (- q) = q )
;- 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;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

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