theorem Th28: :: REVROT_1:28

for p being Point of (TOP-REAL 2)
for f being non empty circular FinSequence of (TOP-REAL 2) holds GoB (Rotate (f,p)) = GoB f