let seq be Real_Sequence; :: thesis: ( seq is non-decreasing & seq is bounded_above implies lim seq = upper_bound seq )
assume A1: ( seq is non-decreasing & seq is bounded_above ) ; :: thesis: lim seq = upper_bound seq
then for n being Nat holds seq . n <= lim seq by SEQ_4:37;
then A2: upper_bound seq <= lim seq by Th9;
for n being Nat holds seq . n <= upper_bound seq by A1, Th7;
then lim seq <= upper_bound seq by A1, PREPOWER:2;
hence lim seq = upper_bound seq by A2, XXREAL_0:1; :: thesis: verum