let k, i, j be natural Number ; :: thesis: ( i <= j + k implies i -' k <= j )
assume i <= j + k ; :: thesis: i -' k <= j
then i -' k <= (j + k) -' k by Th42;
hence i -' k <= j by Th34; :: thesis: verum