for n being Element of NAT
for r being non negative Real
for s, t, x being Point of (TOP-REAL n) st s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) holds
ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) )