:: deftheorem defines convergent_to_+infty MESFUNC5:def 9 :
for seq being ExtREAL_sequence holds
( seq is convergent_to_+infty iff for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m );