theorem :: SPPOL_1:2

for n, k, m being Nat st 1 <= k - m & k - m <= n holds
( k - m in Seg n & k - m is Element of NAT )