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, Def5;
then A4: rseq is bounded_above by Th12;
then lim rseq = lim_inf rseq by A2, RINFSUP1:91;
then lim rseq = upper_bound rseq by A2, RINFSUP1:66;
then A5: lim seq = upper_bound rseq by A2, A4, Th14;
rng seq is bounded_above by A3, Def4;
hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq ) by A2, A4, A5, Th1, Th14; :: thesis: verum