let i, k, m, n be Nat; ( m + k <= i & i <= n + k implies ex mn being Nat st
( mn + k = i & m <= mn & mn <= n ) )
assume that
A1:
m + k <= i
and
A2:
i <= n + k
; ex mn being Nat st
( mn + k = i & m <= mn & mn <= n )
m + k <= m + i
by A1, XREAL_1:38;
then
k <= i
by XREAL_1:6;
then reconsider mn = i - k as Nat by NAT_1:21;
take
mn
; ( mn + k = i & m <= mn & mn <= n )
thus
mn + k = i
; ( m <= mn & mn <= n )
m + k <= mn + k
by A1;
hence
( m <= mn & mn <= n )
by A2, XREAL_1:6; verum