let seq be Real_Sequence; :: thesis: ( seq is non-decreasing & seq is bounded_above implies lower_bound (superior_realsequence seq) = upper_bound seq )
assume A1: ( seq is non-decreasing & seq is bounded_above ) ; :: thesis: lower_bound (superior_realsequence seq) = upper_bound seq
then superior_realsequence seq is constant by Th67;
then consider r1 being Element of REAL such that
A2: rng (superior_realsequence seq) = {r1} by FUNCT_2:111;
r1 in rng (superior_realsequence seq) by A2, TARSKI:def 1;
then ex n being Element of NAT st r1 = (superior_realsequence seq) . n by FUNCT_2:113;
then rng (superior_realsequence seq) = {(upper_bound seq)} by A1, A2, Th67;
hence lower_bound (superior_realsequence seq) = upper_bound seq by SEQ_4:9; :: thesis: verum