for A, B being non empty bounded_above Subset of REAL holds upper_bound (A \/ B) = max ((upper_bound A),(upper_bound B))