let m, k, n be Nat; :: thesis: ( ( m + 1 <= k & k <= n ) iff ex i being Nat st
( m <= i & i < n & k = i + 1 ) )

hereby :: thesis: ( ex i being Nat st
( m <= i & i < n & k = i + 1 ) implies ( m + 1 <= k & k <= n ) )

reconsider a19 = 1 as Integer ;
reconsider k9 = k as Integer ;
assume that
A1: m + 1 <= k and
A2: k <= n ; :: thesis: ex i being Nat st
( m <= i & i < n & k = i + 1 )
1 <= m + 1 by NAT_1:11;
then k9 - a19 in NAT by A1, INT_1:5, XXREAL_0:2;
then reconsider i = k9 - a19 as Nat ;
take i = i; :: thesis: ( m <= i & i < n & k = i + 1 )
(m + 1) - 1 <= k - 1 by A1, XREAL_1:9;
hence m <= i ; :: thesis: ( i < n & k = i + 1 )
k < k + 1 by NAT_1:13;
then k - 1 < (k + 1) - 1 by XREAL_1:9;
hence i < n by A2, XXREAL_0:2; :: thesis: k = i + 1
thus k = i + 1 ; :: thesis: verum

end;

given i being Nat such that A3: m <= i and
A4: i < n and
A5: k = i + 1 ; :: thesis: ( m + 1 <= k & k <= n )
thus ( m + 1 <= k & k <= n ) by A3, A4, A5, NAT_1:13, XREAL_1:7; :: thesis: verum