theorem Th9: :: SPRECT_5:9

for f being constant standard special_circular_sequence
for p, q being Point of (TOP-REAL 2) st p in rng f & q in rng f & p .. f < q .. f holds
p .. (Rotate (f,q)) = ((len f) + (p .. f)) - (q .. f)