:: deftheorem defines lower_bound RINFSUP1:def 2 :
for seq being Real_Sequence holds lower_bound seq = lower_bound (rng seq);