let r be Real; :: thesis: lower_bound {r} = upper_bound {r}
lower_bound {r} = r by XXREAL_2:13;
hence lower_bound {r} = upper_bound {r} by XXREAL_2:11; :: thesis: verum