let seq be ExtREAL_sequence; :: thesis: ( lim_inf seq = lim_sup seq & lim_inf seq = -infty implies ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) )
assume that
A1: lim_inf seq = lim_sup seq and
A2: lim_inf seq = -infty ; :: thesis: ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
A3: superior_realsequence seq is convergent_to_-infty by A1, A2, Th34;
now :: thesis: for g being Real st g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g
let g be Real; :: thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g )

assume g < 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g

then consider n being Nat such that
A4: for m being Nat st n <= m holds
() . m <= g by ;
now :: thesis: for m being Nat st n <= m holds
seq . m <= g
let m be Nat; :: thesis: ( n <= m implies seq . m <= g )
A5: seq . m <= () . m by Th8;
assume n <= m ; :: thesis: seq . m <= g
then (superior_realsequence seq) . m <= g by A4;
hence seq . m <= g by ; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g ; :: thesis: verum
end;
then A6: seq is convergent_to_-infty by MESFUNC5:def 10;
then seq is convergent by MESFUNC5:def 11;
hence ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) by ; :: thesis: verum