for r being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
( Rotation (i,j,n,r) is Orthogonal & (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r)) )