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

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