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 that
A1: seq is bounded and
A2: seq is non-decreasing ; :: thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq )
reconsider rseq = seq as Real_Sequence by A1, Th11;
A3: seq is bounded_above by A1;
then A4: rseq is V70() by Th12;
then lim rseq = lim_inf rseq by A2, RINFSUP1:89;
then lim rseq = upper_bound rseq by A2, RINFSUP1:64;
then A5: lim seq = upper_bound rseq by A2, A4, Th14;
rng seq is bounded_above by A3;
hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq ) by A2, A4, A5, Th1, Th14; :: thesis: verum