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: - X is bounded_below by A1, PSCOMP_1:15;
- Y is bounded_below by A2, PSCOMP_1:15;
then (- X) + (- Y) is bounded_below by A3, COMPLSP1:95;
then - (X + Y) is bounded_below by Th52;
hence X + Y is bounded_above by PSCOMP_1:15; :: thesis: verum