theorem Th5: :: JORDAN1I:5

for f being constant standard special_circular_sequence
for p being Point of (TOP-REAL 2) st p in rng f holds
right_cell (f,(p .. f)) = right_cell ((Rotate (f,p)),1)