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 ) )

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

( 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 ) )

given i being Nat such that A3:
m <= i
and ( 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;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

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