theorem Th26: :: REVROT_1:26

for p being Point of (TOP-REAL 2)
for f being circular FinSequence of (TOP-REAL 2) holds Incr (X_axis f) = Incr (X_axis (Rotate (f,p)))