:: deftheorem defines are_antipodals_of BORSUK_7:def 12 :
for n being Nat
for p, x, y being Point of (TOP-REAL n)
for r being Real
for f being Function holds
( x,y are_antipodals_of p,r,f iff ( x,y are_antipodals_of p,r & x in dom f & y in dom f & f . x = f . y ) );