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 & i = (j -' k) + l ) ; :: thesis: k = (j -' i) + l
i - l = j - k by A2, XREAL_1:233;
hence k = (j - i) + l
.= (j -' i) + l by A1, XREAL_1:233 ;
:: thesis: verum