:: deftheorem Def3 defines HC BROUWER:def 3 :
for n being non zero Element of NAT
for o, s, t being Point of (TOP-REAL n)
for r being non negative Real st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds
for b₆ being Point of (TOP-REAL n) holds
( b₆ = HC (s,t,o,r) iff ( b₆ in (halfline (s,t)) /\ (Sphere (o,r)) & b₆ <> s ) );