theorem Th25: :: IRRAT_1:25

for x being Real
for seq being Real_Sequence st seq is convergent & lim seq = x holds
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