let i, j, k be Nat; :: thesis: (i -' j) -' k = i -' (j + k)

per cases ( i <= j or ( j <= i & i - j <= k ) or ( j <= i & k <= i - j ) ) ;

suppose A1: i <= j ; :: thesis: (i -' j) -' k = i -' (j + k)

hence (i -' j) -' k = 0 -' k by Th8
.= 0 by Th8
.= i -' (j + k) by A1, Th8, NAT_1:12 ;
:: thesis: verum

end;

suppose A2: ( j <= i & i - j <= k ) ; :: thesis: (i -' j) -' k = i -' (j + k)

then A3: i <= j + k by XREAL_1:20;
i -' j = i - j by A2, XREAL_1:233;
hence (i -' j) -' k = 0 by A2, Th8
.= i -' (j + k) by A3, Th8 ;
:: thesis: verum

end;

suppose A4: ( j <= i & k <= i - j ) ; :: thesis: (i -' j) -' k = i -' (j + k)

then A5: k + j <= i by XREAL_1:19;
i -' j = i - j by A4, XREAL_1:233;
hence (i -' j) -' k = (i - j) - k by A4, XREAL_1:233
.= i - (j + k)
.= i -' (j + k) by A5, XREAL_1:233 ;
:: thesis: verum

end;

end;