for C being non empty closed_interval Subset of REAL holds lower_bound C <= upper_bound C