let i, k, l, m, n be Nat; :: thesis:
assume that
A1: m <= n and
A2: k <= l and
A3: m + k <= i and
A4: i <= n + l ; :: thesis:

then consider mn being Nat such that
A5: ( mn + k = i & m <= mn & mn <= n ) by A3, Th1;
take mn ; :: thesis:
take k ; :: thesis:
thus ( mn + k = i & m <= mn & mn <= n ) by A5; :: thesis:
thus ( k <= k & k <= l ) by A2; :: thesis:

end;

then consider kl being Nat such that
A6: kl + n = i and
A7: ( k <= kl & kl <= l ) by A4, Th1;
take n ; :: thesis:
take kl ; :: thesis:
thus ( n + kl = i & m <= n & n <= n ) by A1, A6; :: thesis:
thus ( k <= kl & kl <= l ) by A7; :: thesis:

end;