theorem Th54: :: BORSUK_7:64

for n being 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