for a being Real
for r being non negative Real
for n being non zero Element of NAT
for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) holds
HC (s,t,o,r) = ((1 - a) * s) + (a * t)