let x, y be ExtInt; :: thesis: ( x < y implies x + 1 <= y )
assume A1: x < y ; :: thesis: x + 1 <= y

per cases ( ( x in REAL & y in REAL ) or not x in REAL or not y in REAL ) ;

suppose ( x in REAL & y in REAL ) ; :: thesis: x + 1 <= y

then reconsider x1 = x, y1 = y as Real ;
ex p, q being Real st
( p = x + 1. & q = y & p <= q )

proof

take x1 + 1 ; :: thesis: ex q being Real st
( x1 + 1 = x + 1. & q = y & x1 + 1 <= q )
take y1 ; :: thesis: ( x1 + 1 = x + 1. & y1 = y & x1 + 1 <= y1 )
thus x1 + 1 = x + 1. by XXREAL_3:def 2; :: thesis: ( y1 = y & x1 + 1 <= y1 )
thus y1 = y ; :: thesis: x1 + 1 <= y1
thus x1 + 1 <= y1 by A1, INT_1:7; :: thesis: verum

end;

hence x + 1 <= y ; :: thesis: verum

end;

suppose ( not x in REAL or not y in REAL ) ; :: thesis: x + 1 <= y

then ( x = +infty or x = -infty or y = +infty or y = -infty ) by XXREAL_0:14;
hence x + 1 <= y by A1, XXREAL_0:3; :: thesis: verum

end;

end;