let m be Nat; 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; 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); ( p in Ball (q,r) iff - p in Ball ((- q),r) )
( - (- p) = p & - (- q) = q )
;
hence
( p in Ball (q,r) iff - p in Ball ((- q),r) )
by A1; verum