theorem Th67: :: PREPOWER:67

for a being Real ex s being Rational_Sequence st
( s is convergent & lim s = a & ( for n being Nat holds s . n <= a ) )