let seq be Real_Sequence; :: thesis: ( seq is convergent implies ( lim seq = lim_sup seq & lim seq = lim_inf seq ) )
reconsider r = lim seq as Real ;
assume A1: seq is convergent ; :: thesis: ( lim seq = lim_sup seq & lim seq = lim_inf seq )
then A2: upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) by Th55;
A3: seq is bounded by A1;
then A4: ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by Th56;
A5: for p being Real st 0 < p holds
( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p )

proof

let p be Real; :: thesis: ( 0 < p implies ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) )
assume 0 < p ; :: thesis: ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p )
then consider k being Nat such that
A6: for m being Nat st k <= m holds
|.((seq . m) - r).| < p by A1, SEQ_2:def 7;
A7: for m being Nat st k <= m holds
( r - p <= seq . m & seq . m <= r + p )

proof

let m be Nat; :: thesis: ( k <= m implies ( r - p <= seq . m & seq . m <= r + p ) )
assume k <= m ; :: thesis: ( r - p <= seq . m & seq . m <= r + p )
then |.((seq . m) - r).| < p by A6;
hence ( r - p <= seq . m & seq . m <= r + p ) by Th1; :: thesis: verum

end;

then for m being Nat st k <= m holds
r - p <= seq . m ;
then A8: r - p <= (inferior_realsequence seq) . k by A3, Th43;
for m being Nat st k <= m holds
seq . m <= r + p by A7;
then A9: (superior_realsequence seq) . k <= r + p by A3, Th45;
( (inferior_realsequence seq) . k <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= (superior_realsequence seq) . k ) by A4, Th7, Th8;
hence ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) by A8, A9, XXREAL_0:2; :: thesis: verum

end;

A10: for p being Real st 0 < p holds
r <= (upper_bound (inferior_realsequence seq)) + p

proof

let p be Real; :: thesis: ( 0 < p implies r <= (upper_bound (inferior_realsequence seq)) + p )
assume 0 < p ; :: thesis: r <= (upper_bound (inferior_realsequence seq)) + p
then r - p <= upper_bound (inferior_realsequence seq) by A5;
hence r <= (upper_bound (inferior_realsequence seq)) + p by XREAL_1:20; :: thesis: verum

end;

then A11: r <= upper_bound (inferior_realsequence seq) by XREAL_1:41;
r <= upper_bound (inferior_realsequence seq) by A10, XREAL_1:41;
then A12: r <= lower_bound (superior_realsequence seq) by A2, XXREAL_0:2;
for p being Real st 0 < p holds
lower_bound (superior_realsequence seq) <= r + p by A5;
then A13: lower_bound (superior_realsequence seq) <= r by XREAL_1:41;
then upper_bound (inferior_realsequence seq) <= r by A2, XXREAL_0:2;
hence ( lim seq = lim_sup seq & lim seq = lim_inf seq ) by A13, A11, A12, XXREAL_0:1; :: thesis: verum