let k, i, j be natural Number ; :: thesis: ( i <= j -' k & k <= j implies i + k <= j )
assume that
A1: i <= j -' k and
A2: j >= k ; :: thesis: i + k <= j
i + k <= (j -' k) + k by A1, XREAL_1:6;
hence i + k <= j by A2, XREAL_1:235; :: thesis: verum