theorem Th1: :: NUMBER08:1

for x, y being Nat st x < y & y < x + 2 holds
y = x + 1