let seq be Real_Sequence; :: thesis: ( seq is non-increasing & seq is bounded_below implies sup (inferior_realsequence seq) = inf seq )
assume A1: ( seq is non-increasing & seq is bounded_below ) ; :: thesis: sup (inferior_realsequence seq) = inf seq
then inferior_realsequence seq is V8() by Th75;
then consider r1 being Real such that
A2: rng (inferior_realsequence seq) = {r1} by FUNCT_2:188;
r1 in rng (inferior_realsequence seq) by A2, TARSKI:def 1;
then ex n being Element of NAT st r1 = (inferior_realsequence seq) . n by FUNCT_2:190;
then sup (inferior_realsequence seq) = sup {(inf seq)} by A1, A2, Th75
.= inf seq by SEQ_4:22 ;
hence sup (inferior_realsequence seq) = inf seq ; :: thesis: verum