:: deftheorem defines upper_bound RINFSUP1:def 1 :
for seq being Real_Sequence holds upper_bound seq = upper_bound (rng seq);