let seq be Real_Sequence; :: thesis: ( seq is non-increasing & seq is bounded_below implies lim seq = lower_bound seq )
assume A1: ( seq is non-increasing & seq is bounded_below ) ; :: thesis: lim seq = lower_bound seq
then for n being Nat holds lim seq <= seq . n by SEQ_4:38;
then A2: lim seq <= lower_bound seq by Th10;
for n being Nat holds lower_bound seq <= seq . n by A1, Th8;
then lower_bound seq <= lim seq by A1, PREPOWER:1;
hence lim seq = lower_bound seq by A2, XXREAL_0:1; :: thesis: verum