theorem Th7: :: INT_1:7

for i0, i1 being Integer st i0 < i1 holds
i0 + 1 <= i1