:: deftheorem defines inf RINFSUP2:def 2 :
for seq being ExtREAL_sequence holds inf seq = inf (rng seq);