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