for A being non empty closed_interval Subset of REAL holds A = [.(lower_bound A),(upper_bound A).]