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: -- Y is bounded_below by A2, MEASURE6:41;
A4: -- X is bounded_below by A1, MEASURE6:41;
then lower_bound ((-- X) ++ (-- Y)) = (lower_bound (-- X)) + (lower_bound (-- Y)) by A3, SEQ_4:125;
then A5: lower_bound ((-- X) ++ (-- Y)) = (- (upper_bound (-- (-- X)))) + (lower_bound (-- Y)) by A4, MEASURE6:43
.= (- (upper_bound X)) + (- (upper_bound (-- (-- Y)))) by A3, MEASURE6:43
.= - ((upper_bound X) + (upper_bound Y)) ;
A6: (-- X) ++ (-- Y) = -- (X ++ Y) by Th48;
then A7: -- (X ++ Y) is bounded_below by A4, A3, SEQ_4:124;
reconsider XY = X ++ Y as Subset of REAL by MEMBERED:3;
- (upper_bound (-- (-- XY))) = - ((upper_bound X) + (upper_bound Y)) by A6, A5, A7, MEASURE6:43;
then upper_bound XY = (upper_bound X) + (upper_bound Y) ;
hence upper_bound (X ++ Y) = (upper_bound X) + (upper_bound Y) ; :: thesis: verum