let seq be ExtREAL_sequence; :: thesis: ( seq is bounded & seq is non-increasing implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq ) )

assume that

A1: seq is bounded and

A2: seq is non-increasing ; :: thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq )

reconsider rseq = seq as Real_Sequence by A1, Th11;

A3: seq is bounded_below by A1;

then A4: rseq is V71() by Th13;

then lim rseq = lim_sup rseq by A2, RINFSUP1:89;

then lim rseq = lower_bound rseq by A2, RINFSUP1:70;

then A5: lim seq = lower_bound rseq by A2, A4, Th14;

rng seq is bounded_below by A3;

hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq ) by A2, A4, A5, Th3, Th14; :: thesis: verum

assume that

A1: seq is bounded and

A2: seq is non-increasing ; :: thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq )

reconsider rseq = seq as Real_Sequence by A1, Th11;

A3: seq is bounded_below by A1;

then A4: rseq is V71() by Th13;

then lim rseq = lim_sup rseq by A2, RINFSUP1:89;

then lim rseq = lower_bound rseq by A2, RINFSUP1:70;

then A5: lim seq = lower_bound rseq by A2, A4, Th14;

rng seq is bounded_below by A3;

hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq ) by A2, A4, A5, Th3, Th14; :: thesis: verum