:: deftheorem defines divergent_to-infty LIMFUNC1:def 5 :
for seq being Real_Sequence holds
( seq is divergent_to-infty iff for r being Real ex n being Nat st
for m being Nat st n <= m holds
seq . m < r );