theorem Th6: :: RINFSUP1:6

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