theorem :: BORSUK_7:57

for s being Real holds (Rotate s) * (Rotate (- s)) = id (TOP-REAL 2)