:: deftheorem defines lim_inf RINFSUP1:def 7 :
for seq being Real_Sequence holds lim_inf seq = upper_bound (inferior_realsequence seq);