let seq be Real_Sequence; :: thesis: ( seq is non-increasing & seq is bounded_below implies upper_bound (inferior_realsequence seq) = lower_bound seq )
assume A1: ( seq is non-increasing & seq is bounded_below ) ; :: thesis: upper_bound (inferior_realsequence seq) = lower_bound seq
then inferior_realsequence seq is constant by Th73;
then consider r1 being Element of REAL such that
A2: rng (inferior_realsequence seq) = {r1} by FUNCT_2:111;
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:113;
then upper_bound (inferior_realsequence seq) = upper_bound {(lower_bound seq)} by A1, A2, Th73
.= lower_bound seq by SEQ_4:9 ;
hence upper_bound (inferior_realsequence seq) = lower_bound seq ; :: thesis: verum