for i being Integer holds
( i is odd iff ex j being Integer st i = (2 * j) + 1 )