for k, i being Integer st k < i holds
ex j being Element of NAT st
( j = i - k & 1 <= j )