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