let i, j, k 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 Th60;
hence i -' k <= j by Th39; :: thesis: verum