let seq be Real_Sequence; :: thesis: ( seq is V49() & seq is V89() implies lim seq = lower_bound seq )
assume A1: ( seq is V49() & seq is V89() ) ; :: thesis: lim seq = lower_bound seq
then for n being Element of NAT holds lim seq <= seq . n by SEQ_4:38;
then A2: lim seq <= lower_bound seq by Th10;
for n being Element of NAT holds lower_bound seq <= seq . n by A1, Th8;
then lower_bound seq <= lim seq by A1, PREPOWER:1;
hence lim seq = lower_bound seq by A2, XXREAL_0:1; :: thesis: verum