let seq be Real_Sequence; :: thesis: ( ( seq is bounded & lim_sup seq = lim_inf seq ) iff seq is convergent )
thus ( seq is bounded & lim_sup seq = lim_inf seq implies seq is convergent ) :: thesis: ( seq is convergent implies ( seq is bounded & lim_sup seq = lim_inf seq ) )

proof

assume A1: ( seq is bounded & lim_sup seq = lim_inf seq ) ; :: thesis: seq is convergent
A2: ( seq is bounded_above & seq is bounded_below ) by A1;
A3: ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by A1, Th58;
then A4: ( superior_realsequence seq is bounded_above & superior_realsequence seq is bounded_below ) ;
A5: ( inferior_realsequence seq is bounded_above & inferior_realsequence seq is bounded_below ) by A3;
A6: ( superior_realsequence seq is non-increasing & inferior_realsequence seq is non-decreasing ) by A2, Th52, Th53;
reconsider r = inf (superior_realsequence seq) as real number ;
for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s

proof

let s be real number ; :: thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s )
assume A7: 0 < s ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s
consider k1 being Element of NAT such that
A8: r - s < (inferior_realsequence seq) . k1 by A1, A5, A7, Th7;
consider k2 being Element of NAT such that
A9: (superior_realsequence seq) . k2 < r + s by A4, A7, Th8;
reconsider k = max k1,k2 as Element of NAT ;
( k1 <= k & k2 <= k ) by XXREAL_0:25;
then A10: ( (inferior_realsequence seq) . k1 <= (inferior_realsequence seq) . k & (superior_realsequence seq) . k <= (superior_realsequence seq) . k2 ) by A6, SEQM_3:12, SEQM_3:14;
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s

proof

take k ; :: thesis: for m being Element of NAT st k <= m holds
abs ((seq . m) - r) < s
let m be Element of NAT ; :: thesis: ( k <= m implies abs ((seq . m) - r) < s )
assume A11: k <= m ; :: thesis: abs ((seq . m) - r) < s
consider k3 being Nat such that
A12: m = k + k3 by A11, NAT_1:10;
k3 in NAT by ORDINAL1:def 13;
then ( (inferior_realsequence seq) . k <= seq . m & seq . m <= (superior_realsequence seq) . k ) by A2, A12, Th42, Th43;
then ( (inferior_realsequence seq) . k1 <= seq . m & seq . m <= (superior_realsequence seq) . k2 ) by A10, XXREAL_0:2;
then ( r - s < seq . m & seq . m < r + s ) by A8, A9, XXREAL_0:2;
hence abs ((seq . m) - r) < s by Th1; :: thesis: verum

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s ; :: thesis: verum

end;

hence seq is convergent by SEQ_2:def 6; :: thesis: verum

end;

assume A13: seq is convergent ; :: thesis: ( seq is bounded & lim_sup seq = lim_inf seq )
then A14: seq is bounded by SEQ_2:27;
then A15: ( seq is bounded_above & seq is bounded_below ) ;
A16: ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by A14, Th58;
then A17: ( superior_realsequence seq is bounded_above & superior_realsequence seq is bounded_below ) ;
A18: ( inferior_realsequence seq is bounded_above & inferior_realsequence seq is bounded_below ) by A16;
consider r being real number such that
A19: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < p by A13, SEQ_2:def 6;
A20: for p being real number st 0 < p holds
ex n being Element of NAT st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p )

proof

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) )
assume A21: 0 < p ; :: thesis: ex n being Element of NAT st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p )
consider n being Element of NAT such that
A22: for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < p by A19, A21;
A23: for m being Element of NAT st n <= m holds
( r - p <= seq . m & seq . m <= r + p )

proof

let m be Element of NAT ; :: thesis: ( n <= m implies ( r - p <= seq . m & seq . m <= r + p ) )
assume A24: n <= m ; :: thesis: ( r - p <= seq . m & seq . m <= r + p )
abs ((seq . m) - r) < p by A22, A24;
hence ( r - p <= seq . m & seq . m <= r + p ) by Th1; :: thesis: verum

end;

then for m being Element of NAT st n <= m holds
r - p <= seq . m ;
then A25: r - p <= (inferior_realsequence seq) . n by A15, Th45;
for m being Element of NAT st n <= m holds
seq . m <= r + p by A23;
then (superior_realsequence seq) . n <= r + p by A15, Th47;
hence ex n being Element of NAT st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) by A25; :: thesis: verum

end;

A26: for p being real number st 0 < p holds
( r - p <= sup (inferior_realsequence seq) & inf (superior_realsequence seq) <= r + p )

proof

let p be real number ; :: thesis: ( 0 < p implies ( r - p <= sup (inferior_realsequence seq) & inf (superior_realsequence seq) <= r + p ) )
assume A27: 0 < p ; :: thesis: ( r - p <= sup (inferior_realsequence seq) & inf (superior_realsequence seq) <= r + p )
consider n being Element of NAT such that
A28: ( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) by A20, A27;
( (inferior_realsequence seq) . n <= sup (inferior_realsequence seq) & inf (superior_realsequence seq) <= (superior_realsequence seq) . n ) by A17, A18, Th7, Th8;
hence ( r - p <= sup (inferior_realsequence seq) & inf (superior_realsequence seq) <= r + p ) by A28, XXREAL_0:2; :: thesis: verum

end;

reconsider r = r as Real by XREAL_0:def 1;
for p being real number st 0 < p holds
r <= (sup (inferior_realsequence seq)) + p

proof

let p be real number ; :: thesis: ( 0 < p implies r <= (sup (inferior_realsequence seq)) + p )
assume 0 < p ; :: thesis: r <= (sup (inferior_realsequence seq)) + p
then r - p <= sup (inferior_realsequence seq) by A26;
hence r <= (sup (inferior_realsequence seq)) + p by XREAL_1:22; :: thesis: verum

end;

then A29: r <= sup (inferior_realsequence seq) by XREAL_1:43;
for p being real number st 0 < p holds
inf (superior_realsequence seq) <= r + p by A26;
then A30: inf (superior_realsequence seq) <= r by XREAL_1:43;
sup (inferior_realsequence seq) <= inf (superior_realsequence seq) by A13, Th57, SEQ_2:27;
then ( r <= sup (inferior_realsequence seq) & sup (inferior_realsequence seq) <= r & r <= inf (superior_realsequence seq) & inf (superior_realsequence seq) <= r ) by A29, A30, XXREAL_0:2;
then ( r = sup (inferior_realsequence seq) & r = inf (superior_realsequence seq) ) by XXREAL_0:1;
hence ( seq is bounded & lim_sup seq = lim_inf seq ) by A13, SEQ_2:27; :: thesis: verum