for D being non empty bounded_above Subset of REAL holds upper_bound D = upper_bound (Cl D)