theorem Th2: :: PREPOWER:2

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