theorem Th12: :: FINSEQ_3:12

for k, m, n being Nat st k in Seg n & m < k holds
k - m in Seg n