theorem Th5: :: RINFSUP1:5

for seq being Real_Sequence holds
( seq is bounded_above iff rng seq is bounded_above )