theorem :: SEQM_3:14

for Nseq being increasing sequence of NAT
for n being Nat holds n <= Nseq . n