for r being non negative Real
for n being non zero Element of NAT
for s, t, o being Point of (TOP-REAL n) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds
HC (s,t,o,r) is Point of (Tcircle (o,r))