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