let a, b be Real; ( 0 <= a & 1 < b - a implies ex n being Nat st
( a < n & n < b ) )
assume that
A1:
0 <= a
and
A2:
1 < b - a
; ex n being Nat st
( a < n & n < b )
a < [\a/] + 1
by INT_1:29;
then reconsider n = [\a/] + 1 as Element of NAT by A1, INT_1:3;
take
n
; ( a < n & n < b )
thus
a < n
by INT_1:29; n < b
[\a/] <= a
by INT_1:def 6;
then A3:
[\a/] + 1 <= a + 1
by XREAL_1:6;
1 + a < b
by A2, XREAL_1:20;
hence
n < b
by A3, XXREAL_0:2; verum