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 14 :: thesis: not x,y are_antipodals_of p,r,f
not x in dom f ;
hence not x,y are_antipodals_of p,r,f by Def13; :: thesis: verum