for n being Nat st n > 0 holds
( n mod 2 = 0 iff (n -' 1) mod 2 = 1 )