theorem :: MEASURE6:52

for q3 being Real
for X being non empty Subset of REAL st X is bounded_above holds
upper_bound (q3 ++ X) = q3 + (upper_bound X)