theorem Th1: :: PREPOWER:1

for a being Real
for s1 being Real_Sequence st s1 is convergent & ( for n being Nat holds s1 . n >= a ) holds
lim s1 >= a