theorem Th1: :: LIMFUNC2:1

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