for x, y being odd Element of NAT holds
( x < y iff x + 2 <= y )