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

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

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

hence
seq is convergent
; :: thesis: lim seq = x
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;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

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