theorem Th46: :: RINFSUP1:46

for n being Nat
for seq being Real_Sequence st seq is bounded_below holds
(inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))