:: deftheorem Def8 defines RotateCircle JORDAN:def 8 :
for n being non zero Element of NAT
for o, p being Point of (TOP-REAL n)
for r being positive Real st p in Ball (o,r) holds
for b₅ being Function of (Tcircle (o,r)),(Tcircle (o,r)) holds
( b₅ = RotateCircle (o,r,p) iff for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y & b₅ . x = HC (y,p,o,r) ) );