for s being Real
for p being Point of (TOP-REAL 2) holds (Rotate s) . ((Rotate (- s)) . p) = p