for seq being ExtREAL_sequence holds
( seq is convergent iff lim_inf seq = lim_sup seq )