theorem IncFinNAT: :: NUMBER12:9

for n being Nat holds (Seg 1) --> n is increasing FinSequence of NAT