:: deftheorem defines are_antipodals_of BORSUK_7:def 11 :
for n being Nat
for p, x, y being Point of (TOP-REAL n)
for r being Real holds
( x,y are_antipodals_of p,r iff ( x is Point of (Tcircle (p,r)) & y is Point of (Tcircle (p,r)) & p in LSeg (x,y) ) );