let n be non zero Nat; :: thesis: 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; :: thesis: 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); :: thesis: ( 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)) ; :: thesis: 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; :: according to BORSUK_7:def 11 :: thesis: 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)) ; :: thesis: verum