for r being Real holds lower_bound {r} = upper_bound {r}