for n being Nat st n is even holds
n + 1 is odd ;