theorem Th1: :: GLIB_006:1

for n being even Integer
for m being odd Integer st n <= m holds
n + 1 <= m