for seq being ExtREAL_sequence st seq is convergent holds
( lim seq = lim_inf seq & lim seq = lim_sup seq )