for X being non empty Subset of REAL st X is bounded_above holds
upper_bound X = - (lower_bound (-- X))