theorem :: MATRIX13:11
for n being Nat
for R being Element of Permutations n st R = Rev (idseq n) holds
( R is even iff (n choose 2) mod 2 = 0 )