:: deftheorem defines lim_sup RINFSUP2:def 8 :
for seq being ExtREAL_sequence holds lim_sup seq = inf (superior_realsequence seq);