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 V20() 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 upper_bound (inferior_realsequence seq) = upper_bound {(lower_bound seq)} by A1, A2, Th75
.= lower_bound seq by SEQ_4:22 ;
hence upper_bound (inferior_realsequence seq) = lower_bound seq ; :: thesis: verum