theorem :: FINSEQ_3:11

for k, n being Nat st k < n holds
k + 1 in Seg n