let i, j, k, l be Nat; :: thesis: ( i <= j & k <= j & i = (j -' k) + l implies k = (j -' i) + l )
assume that
A1: i <= j and
A2: k <= j and
A3: i = (j -' k) + l ; :: thesis: k = (j -' i) + l
i - l = j - k by A2, A3, XREAL_1:235;
hence k = (j - i) + l
.= (j -' i) + l by A1, XREAL_1:235 ;
:: thesis: verum