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
A1: ( 0 < t & t < s - r ) by XREAL_1:7;
reconsider t = t as Real by XREAL_0:def 1;
A2: 1 / t > 0 by A1, XREAL_1:141;
A3: [/(1 / t)\] + 1 > 1 / t by INT_1:57;
set n = [/(1 / t)\];
reconsider n = [/(1 / t)\] as Element of NAT by A2, A3, INT_1:16, INT_1:20;
(n + 1) * t >= 1 by A1, A3, XREAL_1:83;
then 1 / (n + 1) <= t by XREAL_1:81;
then 1 / (n + 1) < s - r by A1, XXREAL_0:2;
hence ex n being Element of NAT st 1 / (n + 1) < s - r ; :: thesis: verum