for seq being ExtREAL_sequence holds lim_inf seq <= lim_sup seq