theorem Th67: :: JORDAN:67

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
RotateCircle (o,r,p) is without_fixpoints