let x be Real; :: thesis: 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 )

let seq be Real_Sequence; :: thesis: ( ( 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 implies ( seq is convergent & lim seq = x ) )

assume that
A1: 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 and
A2: ex N being Nat st
for n being Nat st n >= N holds
seq . n <= x ; :: thesis: ( seq is convergent & lim seq = x )
A3: 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
proof
let eps be Real; :: thesis: ( eps > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.((seq . n) - x).| < eps )

assume A4: eps > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.((seq . n) - x).| < eps

then A5: x + eps > x + 0 by XREAL_1:6;
consider N2 being Nat such that
A6: for n being Nat st n >= N2 holds
seq . n <= x by A2;
consider N1 being Nat such that
A7: for n being Nat st n >= N1 holds
seq . n > x - eps by A1, A4;
reconsider N = max (N1,N2) as Nat by TARSKI:1;
take N ; :: thesis: for n being Nat st n >= N holds
|.((seq . n) - x).| < eps

let n be Nat; :: thesis: ( n >= N implies |.((seq . n) - x).| < eps )
assume A8: n >= N ; :: thesis: |.((seq . n) - x).| < eps
then n >= N1 by XXREAL_0:30;
then seq . n > x - eps by A7;
then A9: (seq . n) - x > (x - eps) - x by XREAL_1:9;
seq . n <= x by ;
then seq . n < x + eps by ;
then (seq . n) - x < eps by XREAL_1:19;
hence |.((seq . n) - x).| < eps by ; :: thesis: verum
end;
hence seq is convergent ; :: thesis: lim seq = x
hence lim seq = x by ; :: thesis: verum