let k, i, j be natural Number ; :: thesis: ( i < j & k < j implies i -' k < j -' k )
assume that
A1: i < j and
A2: k < j ; :: thesis: i -' k < j -' k

per cases ( k <= i or k > i ) ;

suppose k <= i ; :: thesis: i -' k < j -' k

then A3: i -' k = i - k by XREAL_1:233;
j -' k = j - k by A2, XREAL_1:233;
hence i -' k < j -' k by A1, A3, XREAL_1:9; :: thesis: verum

end;

suppose k > i ; :: thesis: i -' k < j -' k

then i - k < 0 by XREAL_1:49;
then A4: i -' k = 0 by XREAL_0:def 2;
j -' k <> 0 by A2, Th36;
hence i -' k < j -' k by A4; :: thesis: verum

end;

end;