let k be Nat; :: thesis: k / (k + 1) < 1
for m being Nat holds m < m + 1 by XREAL_1:29;
hence k / (k + 1) < 1 by XREAL_1:189; :: thesis: verum