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