let X, Y be Subset of REAL; :: thesis: ( X is bounded_above & Y is bounded_above implies X ++ Y is bounded_above )
assume that
A1: X is bounded_above and
A2: Y is bounded_above ; :: thesis: X ++ Y is bounded_above
A3: -- Y is bounded_below by A2, MEASURE6:41;
-- X is bounded_below by A1, MEASURE6:41;
then A4: (-- X) ++ (-- Y) is bounded_below by A3, SEQ_4:124;
reconsider XY = X ++ Y as Subset of REAL by MEMBERED:3;
-- XY is bounded_below by Th48, A4;
hence X ++ Y is bounded_above by MEASURE6:41; :: thesis: verum