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