let seq be ExtREAL_sequence; :: thesis:
assume that
A1: seq is non-increasing and
A2: -infty = inf seq ; :: thesis:
A3: seq is convergent_to_-infty

proof

assume not seq is convergent_to_-infty ; :: thesis:
then consider g being Real such that
g < 0 and
A4: for n being Nat ex m being Nat st
( n <= m & g < seq . m ) by MESFUNC5:def 10;
for y being ExtReal st y in rng seq holds
g <= y

proof

let y be ExtReal; :: thesis:
assume y in rng seq ; :: thesis:
then consider n being object such that
A5: n in NAT and
A6: y = seq . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A5;
consider m being Nat such that
A7: n <= m and
A8: g < seq . m by A4;
seq . m <= seq . n by A1, A7, Th7;
hence g <= y by A6, A8, XXREAL_0:2; :: thesis:

end;

then g is LowerBound of rng seq by XXREAL_2:def 2;
then A9: g <= inf (rng seq) by XXREAL_2:def 4;
g in REAL by XREAL_0:def 1;
hence contradiction by A2, A9, XXREAL_0:12; :: thesis:

end;

then seq is convergent by MESFUNC5:def 11;
hence ( seq is convergent_to_-infty & lim seq = -infty ) by A3, MESFUNC5:def 12; :: thesis: