for X, Y being non empty Subset of REAL st X is bounded_above & Y is bounded_above holds
upper_bound (X ++ Y) = (upper_bound X) + (upper_bound Y)