let f be Function of (Tcircle (p,r)),(TOP-REAL n); :: thesis: f is without_antipodals
let x, y be Point of (TOP-REAL (n + 1)); :: according to BORSUK_7:def 13 :: thesis: not x,y are_antipodals_of p,r,f
thus not x,y are_antipodals_of p,r,f ; :: thesis: verum