theorem Th10: :: FVALUAT1:10

for x, y being ExtInt st x < y holds
x + 1 <= y