for p, th being Real
for rseq being Real_Sequence st rseq is convergent & lim rseq = th & ( for n being Nat holds rseq . n >= p ) holds
th >= p by PREPOWER:1;