theorem Th38: :: RINFSUP1:38

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