:: deftheorem defines divergent_to+infty LIMFUNC1:def 4 :
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
r < seq . m );