let r, s be Real; :: 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:50;
then consider t being Real such that
A1: 0 < t and
A2: t < s - r by XREAL_1:5;
reconsider t = t as Real ;
A3: 1 / t > 0 by A1, XREAL_1:139;
A4: [/(1 / t)\] + 1 > 1 / t by INT_1:32;
set n = [/(1 / t)\];
reconsider n = [/(1 / t)\] as Element of NAT by A3, A4, INT_1:3, INT_1:7;
(n + 1) * t >= 1 by A1, A4, XREAL_1:81;
then 1 / (n + 1) <= t by XREAL_1:79;
then 1 / (n + 1) < s - r by A2, XXREAL_0:2;
hence ex n being Element of NAT st 1 / (n + 1) < s - r ; :: thesis: verum