for n being Nat ex m being Element of NAT st
( n = 2 * m or n = (2 * m) + 1 )