theorem Th4: :: LIMFUNC1:4

for seq being Real_Sequence st seq is convergent & 0 < lim seq holds
ex n being Nat st
for m being Nat st n <= m holds
0 < seq . m