theorem Th2: :: HEINE:2

for n being Nat
for seq being Real_Sequence st seq is increasing & rng seq c= NAT holds
n <= seq . n