:: deftheorem Def7 defines DiskProj JORDAN:def 7 :
for n being non zero Element of NAT
for o, p being Point of (TOP-REAL n)
for r being positive Real st p is Point of (Tdisk (o,r)) holds
for b₅ being Function of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),(Tcircle (o,r)) holds
( b₅ = DiskProj (o,r,p) iff for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & b₅ . x = HC (p,y,o,r) ) );