let x, y be Nat; :: thesis: ( x < y & y < x + 2 implies y = x + 1 )
assume x < y ; :: thesis: ( not y < x + 2 or y = x + 1 )
then A1: x + 1 <= y by NAT_1:13;
assume y < x + 2 ; :: thesis: y = x + 1
then y < (x + 1) + 1 ;
then y <= x + 1 by NAT_1:13;
hence y = x + 1 by A1, XXREAL_0:1; :: thesis: verum