let seq be Real_Sequence; :: thesis: ( seq is non-decreasing & seq is bounded_above implies inf (superior_realsequence seq) = sup seq )
assume A1: ( seq is non-decreasing & seq is bounded_above ) ; :: thesis: inf (superior_realsequence seq) = sup seq
then superior_realsequence seq is V8() by Th69;
then consider r1 being Real such that
A2: rng (superior_realsequence seq) = {r1} by FUNCT_2:188;
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:190;
then rng (superior_realsequence seq) = {(sup seq)} by A1, A2, Th69;
hence inf (superior_realsequence seq) = sup seq by SEQ_4:22; :: thesis: verum