let r, s be real number ; :: thesis: ( r < s implies ex n being Element of NAT st 1 / (n + 1) < s - r )
assume A1: r < s ; :: thesis: ex n being Element of NAT st 1 / (n + 1) < s - r
A2: s - r > 0 by A1, XREAL_1:52;
consider t being real number such that
A3: 0 < t and
A4: t < s - r by A2, 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;
A7: (n + 1) * t >= 1 by A3, A6, XREAL_1:83;
A8: 1 / (n + 1) <= t by A7, XREAL_1:81;
A9: 1 / (n + 1) < s - r by A4, A8, XXREAL_0:2;
thus ex n being Element of NAT st 1 / (n + 1) < s - r by A9; :: thesis: verum