:: deftheorem defines bounded_above RINFSUP2:def 4 :
for seq being ExtREAL_sequence holds
( seq is bounded_above iff rng seq is bounded_above );