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:77;
-- X is bounded_below by A1, MEASURE6:77;
then A4: (-- X) ++ (-- Y) is bounded_below by A3, SEQ_4:141;
X ++ Y c= REAL by MEMBERED:3;
then reconsider XY = X ++ Y as Subset of REAL ;
-- XY is bounded_below by Th52, A4;
then -- (-- (X ++ Y)) is bounded_above by MEASURE6:77;
hence X ++ Y is bounded_above ; :: thesis: verum