let r, s be Real; :: thesis: ( ( for n being Element of NAT holds r - (1 / (n + 1)) <= s ) implies r <= s )
assume A1: for n being Element of NAT holds r - (1 / (n + 1)) <= s ; :: thesis: r <= s
assume r > s ; :: thesis: contradiction
then consider n being Element of NAT such that
A2: 1 / (n + 1) < r - s by Th10;
s + (1 / (n + 1)) < r by A2, XREAL_1:20;
then s < r - (1 / (n + 1)) by XREAL_1:20;
hence contradiction by A1; :: thesis: verum