let seq be Real_Sequence; :: thesis: ( seq is V55() & seq is V96() implies lim seq = lower_bound seq )
assume A1: ( seq is V55() & seq is V96() ) ; :: thesis: lim seq = lower_bound seq
then for n being Nat holds lim seq <= seq . n by SEQ_4:38;
then A2: lim seq <= lower_bound seq by Th10;
for n being 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