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
(superior_realsequence seq) . m <= g by A3, MESFUNC5:def 10;

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 <= (superior_realsequence seq) . m by Th8;
assume n <= m ; :: thesis: seq . m <= g
then (superior_realsequence seq) . m <= g by A4;
hence seq . m <= g by A5, XXREAL_0:2; :: 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 A1, A2, A6, MESFUNC5:def 12; :: thesis: verum