let seq be Real_Sequence; :: thesis: ( seq is non-increasing & seq is bounded_below implies lim seq = inf seq )
assume A1: ( seq is non-increasing & seq is bounded_below ) ; :: thesis: lim seq = inf seq
then A2: ( seq is bounded & seq is convergent ) by Th23;
then ( seq is bounded_above & seq is bounded_below ) ;
then for n being Element of NAT holds inf seq <= seq . n by Th8;
then A3: inf seq <= lim seq by A2, PREPOWER:2;
for n being Element of NAT holds lim seq <= seq . n by A1, SEQ_4:55;
then lim seq <= inf seq by Th10;
hence lim seq = inf seq by A3, XXREAL_0:1; :: thesis: verum