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 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 ) & 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 )
A2: 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 A3: 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 consider N1 being Element of NAT such that
A4: for n being Element of NAT st n >= N1 holds
seq . n > x - eps by A1;
consider N2 being Element of NAT such that
A5: for n being Element of NAT st n >= N2 holds
seq . n <= x by A1;
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 n >= N ; :: thesis: abs ((seq . n) - x) < eps
then ( n >= N1 & n >= N2 ) by XXREAL_0:30;
then A6: ( seq . n > x - eps & seq . n <= x ) by A4, A5;
then A7: (seq . n) - x > (x - eps) - x by XREAL_1:11;
x + eps > x + 0 by A3, XREAL_1:8;
then seq . n < x + eps by A6, XXREAL_0:2;
then (seq . n) - x < eps by XREAL_1:21;
hence abs ((seq . n) - x) < eps by A7, SEQ_2:9; :: thesis: verum

end;

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