let x be real number ; :: thesis: for seq being Real_Sequence st ( for eps being real number st eps > 0 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
seq . n > x - eps ) & ex N being Element of NAT st
for n being Element of 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 number st eps > 0 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
seq . n > x - eps ) & ex N being Element of NAT st
for n being Element of NAT st n >= N holds
seq . n <= x implies ( seq is convergent & lim seq = x ) )
assume that
A1: for eps being real number st eps > 0 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
seq . n > x - eps and
A2: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
seq . n <= x ; :: thesis: ( seq is convergent & lim seq = x )
A3: for eps being real number st eps > 0 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((seq . n) - x) < eps

proof

let eps be real number ; :: thesis: ( eps > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((seq . n) - x) < eps )
assume A4: eps > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((seq . n) - x) < eps
then A5: x + eps > x + 0 by XREAL_1:6;
consider N2 being Element of NAT such that
A6: for n being Element of NAT st n >= N2 holds
seq . n <= x by A2;
consider N1 being Element of NAT such that
A7: for n being Element of NAT st n >= N1 holds
seq . n > x - eps by A1, A4;
take N = max (N1,N2); :: thesis: for n being Element of NAT st n >= N holds
abs ((seq . n) - x) < eps
let n be Element of NAT ; :: thesis: ( n >= N implies abs ((seq . n) - x) < eps )
assume A8: n >= N ; :: thesis: abs ((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 abs ((seq . n) - x) < eps by A9, SEQ_2:1; :: thesis: verum

end;

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