theorem Th5: :: JORDAN24:5

for z being Complex
for r being Real holds Rotate (z,(- r)) = Rotate (z,((2 * PI) - r))