let m, k, n be Nat; :: thesis:

reconsider a19 = 1 as Integer ;
reconsider k9 = k as Integer ;
assume that
A1: m + 1 <= k and
A2: k <= n ; :: thesis:
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 + 1) - 1 <= k - 1 by A1, XREAL_1:9;
hence m <= i ; :: thesis:
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:
thus k = i + 1 ; :: thesis:

end;

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