for n being Nat
for PERM being Permutation of (Permutations n)
for perm being Element of Permutations n st perm is odd & ( for p being Element of Permutations n holds PERM . p = p * perm ) holds
PERM .: { p where p is Element of Permutations n : p is even } = { q where q is Element of Permutations n : q is odd }