theorem Th73: :: RINFSUP1:73

for n being Nat
for seq being Real_Sequence st seq is non-increasing & seq is bounded_below holds
( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant )