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