for n being Nat holds
( n is odd iff ex k being Nat st n = (2 * k) + 1 )