let r be Real; :: thesis: 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)) )
let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies ( Rotation (i,j,n,r) is Orthogonal & (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r)) ) )
assume ( 1 <= i & i < j & j <= n ) ; :: thesis: ( Rotation (i,j,n,r) is Orthogonal & (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r)) )
then ( (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r)) & (Rotation (i,j,n,r)) @ = Rotation (i,j,n,(- r)) ) by Lm4, Lm5;
hence ( Rotation (i,j,n,r) is Orthogonal & (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r)) ) by MATRIX_6:def 7; :: thesis: verum