theorem Th56: :: RINFSUP1:56

for seq being Real_Sequence st seq is bounded holds
( superior_realsequence seq is bounded & inferior_realsequence seq is bounded )