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 for n being Element of NAT holds lim seq <= seq . n by SEQ_4:55;
then A2: lim seq <= inf seq by Th10;
for n being Element of NAT holds inf seq <= seq . n by A1, Th8;
then inf seq <= lim seq by A1, PREPOWER:2;
hence lim seq = inf seq by A2, XXREAL_0:1; :: thesis: verum