for x being Real for seq being Real_Sequence st ( for eps being Real st eps >0 holds ex N being Nat st for n being Nat st n >= N holds seq . n > x - eps ) & ex N being Nat st for n being Nat st n >= N holds seq . n <= x holds ( seq is convergent & lim seq = x )