let n, k, m be Nat; :: thesis: ( 1 <= k - m & k - m <= n implies ( k - m in Seg n & k - m is Element of NAT ) )
assume that
A1: 1 <= k - m and
A2: k - m <= n ; :: thesis: ( k - m in Seg n & k - m is Element of NAT )
k - m is Element of NAT by A1, INT_1:3;
hence ( k - m in Seg n & k - m is Element of NAT ) by A1, A2, FINSEQ_1:1; :: thesis: verum