theorem Th38: :: RINFSUP1:38

for seq being Real_Sequence st seq is V96() holds
(inferior_realsequence seq) . 0 = lower_bound seq