theorem Th55: :: RINFSUP1:55

for seq being Real_Sequence st seq is bounded holds
upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq)