let n be non zero Nat; for r being non negative Real
for x being Point of (TOP-REAL n) st x is Point of (Tcircle ((0. (TOP-REAL n)),r)) holds
x, - x are_antipodals_of 0. (TOP-REAL n),r
let r be non negative Real; for x being Point of (TOP-REAL n) st x is Point of (Tcircle ((0. (TOP-REAL n)),r)) holds
x, - x are_antipodals_of 0. (TOP-REAL n),r
let x be Point of (TOP-REAL n); ( x is Point of (Tcircle ((0. (TOP-REAL n)),r)) implies x, - x are_antipodals_of 0. (TOP-REAL n),r )
assume A1:
x is Point of (Tcircle ((0. (TOP-REAL n)),r))
; x, - x are_antipodals_of 0. (TOP-REAL n),r
reconsider y = x as Point of (Tcircle ((0. (TOP-REAL n)),r)) by A1;
- x = - y
;
hence
( x is Point of (Tcircle ((0. (TOP-REAL n)),r)) & - x is Point of (Tcircle ((0. (TOP-REAL n)),r)) )
by TOPREALC:60; BORSUK_7:def 11 0. (TOP-REAL n) in LSeg (x,(- x))
((1 - (1 / 2)) * x) + ((1 / 2) * (- x)) =
((1 / 2) * x) + (- ((1 / 2) * x))
by RLVECT_1:25
.=
0. (TOP-REAL n)
by RLVECT_1:5
;
hence
0. (TOP-REAL n) in LSeg (x,(- x))
; verum