let seq be Real_Sequence; :: thesis: ( seq is bounded implies ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) )
assume A1: seq is bounded ; :: thesis: ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded )
then ( seq is bounded_above & seq is bounded_below ) ;
then ( superior_realsequence seq is non-increasing & inferior_realsequence seq is non-decreasing ) by Th52, Th53;
then A2: ( superior_realsequence seq is bounded_above & inferior_realsequence seq is bounded_below ) by LIMFUNC1:26;

now

let m be Element of NAT ; :: thesis: (inferior_realsequence seq) . m < (inf (superior_realsequence seq)) + 1
(inferior_realsequence seq) . m <= inf (superior_realsequence seq) by A1, Th55;
hence (inferior_realsequence seq) . m < (inf (superior_realsequence seq)) + 1 by Lm1; :: thesis: verum

end;

then A3: inferior_realsequence seq is bounded_above by SEQ_2:def 3;

now

let m be Element of NAT ; :: thesis: (sup (inferior_realsequence seq)) - 1 < (superior_realsequence seq) . m
sup (inferior_realsequence seq) <= (superior_realsequence seq) . m by A1, Th56;
hence (sup (inferior_realsequence seq)) - 1 < (superior_realsequence seq) . m by Lm1; :: thesis: verum

end;

then superior_realsequence seq is bounded_below by SEQ_2:def 4;
hence ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by A2, A3; :: thesis: verum