:: deftheorem defines sup RINFSUP2:def 1 :
for seq being ExtREAL_sequence holds sup seq = sup (rng seq);