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, Def5;
then A4: rseq is bounded_below 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, Def3;
hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq ) by A2, A4, A5, Th3, Th14; :: thesis: verum