let r, s be real number ; :: 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 A2: r > s ; :: thesis: contradiction
consider n being Element of NAT such that
A3: 1 / (n + 1) < r - s by A2, Th13;
A4: s + (1 / (n + 1)) < r by A3, XREAL_1:22;
A5: s < r - (1 / (n + 1)) by A4, XREAL_1:22;
thus contradiction by A1, A5; :: thesis: verum