theorem Th53: :: RINFSUP1:53

for n being Nat
for seq being Real_Sequence st seq is bounded holds
(inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq)