theorem Th8: :: NAT_1:8

for i, j being natural Number holds
( not i <= j + 1 or i <= j or i = j + 1 )