:: deftheorem defines lim_sup RINFSUP1:def 6 :
for seq being Real_Sequence holds lim_sup seq = lower_bound (superior_realsequence seq);