theorem Th1: :: GLIB_001:1

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