for seq being ExtREAL_sequence st ( for n being Element of NAT holds +infty <= seq . n ) holds
seq is convergent_to_+infty