let seq be ExtREAL_sequence; :: thesis: ( seq is bounded & seq is non-decreasing implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq ) )
assume A1: ( seq is bounded & seq is non-decreasing ) ; :: thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq )
then reconsider rseq = seq as Real_Sequence by Th11;
A2: seq is bounded_above by A1, Def5;
then A3: rseq is bounded_above by Th12;
A5: rseq is convergent by A3, A1;
then lim rseq = lim_inf rseq by RINFSUP1:91;
then lim rseq = sup rseq by A1, RINFSUP1:66;
then A6: lim seq = sup rseq by A5, Th14;
rng seq is bounded_above by A2, Def4;
hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq ) by A5, A6, Th1, Th14; :: thesis: verum