for n being Nat
for IT being Element of Permutations n st n >= 1 holds
( IT is even iff IT " is even )