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 A6, A8, XXREAL_0:30;
then seq . n < x + eps by A5, XXREAL_0:2;
then (seq . n) - x < eps by XREAL_1:19;
hence |.((seq . n) - x).| < eps by A9, SEQ_2:1; :: thesis: verum

end;

hence seq is convergent ; :: thesis: lim seq = x
hence lim seq = x by A3, SEQ_2:def 7; :: thesis: verum