:: deftheorem defines lim_inf RINFSUP2:def 9 :
for seq being ExtREAL_sequence holds lim_inf seq = sup (inferior_realsequence seq);