let seq be ExtREAL_sequence; :: thesis: ( ( for n being Element of NAT holds seq . n <= -infty ) implies seq is convergent_to_-infty )
assume A1: for n being Element of NAT holds seq . n <= -infty ; :: thesis: seq is convergent_to_-infty
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
now :: thesis: for m being Nat st 0 <= m holds
seq . m <= g
let m be Nat; :: thesis: ( 0 <= m implies seq . m <= g )
assume 0 <= m ; :: thesis: seq . m <= g
m is Element of NAT by ORDINAL1:def 12;
then A2: seq . m <= -infty by A1;
-infty <= g by XXREAL_0:5;
hence seq . m <= g by A2, 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;
hence seq is convergent_to_-infty by MESFUNC5:def 10; :: thesis: verum