:: deftheorem defines bounded RINFSUP2:def 5 :
for seq being ExtREAL_sequence holds
( seq is bounded iff ( seq is bounded_above & seq is bounded_below ) );