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 inferior_realsequence seq is non-decreasing by Th52;
then A2: inferior_realsequence seq is bounded_below by LIMFUNC1:1;

now

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

end;

then A3: superior_realsequence seq is bounded_below by SEQ_2:def 4;

now

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

end;

then A4: inferior_realsequence seq is bounded_above by SEQ_2:def 3;
superior_realsequence seq is non-increasing by A1, Th53;
then superior_realsequence seq is bounded_above by LIMFUNC1:1;
hence ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by A2, A4, A3; :: thesis: verum