theorem Th6: :: RINFSUP1:6

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