let seq be Real_Sequence; :: thesis: ( seq is convergent implies ( lim seq = lim_sup seq & lim seq = lim_inf seq ) )
assume A1: seq is convergent ; :: thesis: ( lim seq = lim_sup seq & lim seq = lim_inf seq )
then A2: seq is bounded by SEQ_2:27;
then A3: ( seq is bounded_above & seq is bounded_below ) ;
A4: ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by A2, Th58;
then A5: ( superior_realsequence seq is bounded_above & superior_realsequence seq is bounded_below ) ;
A6: ( inferior_realsequence seq is bounded_above & inferior_realsequence seq is bounded_below ) by A4;
reconsider r = lim seq as real number ;
A7: 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 A8: 0 < p ; :: thesis: ( r - p <= sup (inferior_realsequence seq) & inf (superior_realsequence seq) <= r + p )
consider k being Element of NAT such that
A9: for m being Element of NAT st k <= m holds
abs ((seq . m) - r) < p by A1, A8, SEQ_2:def 7;
A10: for m being Element of NAT st k <= m holds
( r - p <= seq . m & seq . m <= r + p )

proof

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

end;

then for m being Element of NAT st k <= m holds
r - p <= seq . m ;
then A12: r - p <= (inferior_realsequence seq) . k by A3, Th45;
for m being Element of NAT st k <= m holds
seq . m <= r + p by A10;
then A13: (superior_realsequence seq) . k <= r + p by A3, Th47;
( (inferior_realsequence seq) . k <= sup (inferior_realsequence seq) & inf (superior_realsequence seq) <= (superior_realsequence seq) . k ) by A5, A6, Th7, Th8;
hence ( r - p <= sup (inferior_realsequence seq) & inf (superior_realsequence seq) <= r + p ) by A12, A13, XXREAL_0:2; :: thesis: verum

end;

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 A7;
hence r <= (sup (inferior_realsequence seq)) + p by XREAL_1:22; :: thesis: verum

end;

then A14: 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 A7;
then A15: inf (superior_realsequence seq) <= r by XREAL_1:43;
sup (inferior_realsequence seq) <= inf (superior_realsequence seq) by A1, 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 A14, A15, XXREAL_0:2;
hence ( lim seq = lim_sup seq & lim seq = lim_inf seq ) by XXREAL_0:1; :: thesis: verum