:: deftheorem defines with_antipodals BORSUK_7:def 13 :
for m, n being Nat
for p being Point of (TOP-REAL m)
for r being Real
for f being Function of (Tcircle (p,r)),(TOP-REAL n) holds
( f is with_antipodals iff ex x, y being Point of (TOP-REAL m) st x,y are_antipodals_of p,r,f );