theorem :: RINFSUP2:39

for seq being ExtREAL_sequence holds lim_inf seq <= lim_sup seq