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 A2: ( seq is bounded & seq is convergent ) by Th22;
then ( seq is bounded_above & seq is bounded_below ) ;
then for n being Element of NAT holds seq . n <= sup seq by Th7;
then A3: lim seq <= sup seq by A2, PREPOWER:3;
for n being Element of NAT holds seq . n <= lim seq by A1, SEQ_4:54;
then sup seq <= lim seq by Th9;
hence lim seq = sup seq by A3, XXREAL_0:1; :: thesis: verum