let X, Y be non empty Subset of REAL ; :: thesis: ( X is bounded_above & Y is bounded_above implies upper_bound (X + Y) = (upper_bound X) + (upper_bound Y) )
assume that
A1: X is bounded_above and
A2: Y is bounded_above ; :: thesis: upper_bound (X + Y) = (upper_bound X) + (upper_bound Y)
A3: (- X) + (- Y) = - (X + Y) by Th52;
then A4: not - (X + Y) is empty by COMPLSP1:94;
A5: - X is bounded_below by A1, PSCOMP_1:15;
A6: - Y is bounded_below by A2, PSCOMP_1:15;
then A7: - (X + Y) is bounded_below by A3, A5, COMPLSP1:95;
lower_bound ((- X) + (- Y)) = (lower_bound (- X)) + (lower_bound (- Y)) by A5, A6, COMPLSP1:96;
then lower_bound ((- X) + (- Y)) = (- (upper_bound (- (- X)))) + (lower_bound (- Y)) by A5, PSCOMP_1:17
.= (- (upper_bound X)) + (- (upper_bound (- (- Y)))) by A6, PSCOMP_1:17
.= - ((upper_bound X) + (upper_bound Y)) ;
then - (upper_bound (- (- (X + Y)))) = - ((upper_bound X) + (upper_bound Y)) by A3, A4, A7, PSCOMP_1:17;
hence upper_bound (X + Y) = (upper_bound X) + (upper_bound Y) ; :: thesis: verum