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