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

assume A1: x < y ; :: thesis: 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 )
;

end;

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 )

end;ex p, q being Real st

( p = x + 1. & q = y & p <= q )

proof

hence
x + 1 <= y
; :: thesis: verum
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;( 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