let r, s be real number ; :: thesis: ( r < s implies ex n being Element of NAT st 1 / (n + 1) < s - r )
assume r < s ; :: thesis: ex n being Element of NAT st 1 / (n + 1) < s - r
then s - r > 0 by XREAL_1:52;
then consider t being real number such that
A3: 0 < t and
A4: t < s - r by XREAL_1:7;
reconsider t = t as Real by XREAL_0:def 1;
A5: 1 / t > 0 by A3, XREAL_1:141;
A6: [/(1 / t)\] + 1 > 1 / t by INT_1:57;
set n = [/(1 / t)\];
reconsider n = [/(1 / t)\] as Element of NAT by A5, A6, INT_1:16, INT_1:20;
(n + 1) * t >= 1 by A3, A6, XREAL_1:83;
then 1 / (n + 1) <= t by XREAL_1:81;
then 1 / (n + 1) < s - r by A4, XXREAL_0:2;
hence ex n being Element of NAT st 1 / (n + 1) < s - r ; :: thesis: verum