let seq be Real_Sequence; :: thesis: ( seq is non-decreasing & seq is bounded_above implies lim seq = sup seq )
assume A1: ( seq is non-decreasing & seq is bounded_above ) ; :: thesis: lim seq = sup seq
then for n being Element of NAT holds seq . n <= lim seq by SEQ_4:54;
then A2: sup seq <= lim seq by Th9;
for n being Element of NAT holds seq . n <= sup seq by A1, Th7;
then lim seq <= sup seq by A1, PREPOWER:3;
hence lim seq = sup seq by A2, XXREAL_0:1; :: thesis: verum