theorem Th2: :: LIMFUNC2:2

for r being Real
for seq being Real_Sequence st seq is convergent & lim seq < r holds
ex n being Nat st
for k being Nat st n <= k holds
seq . k < r