let r be real number ; :: thesis: lower_bound {r} = upper_bound {r}
( lower_bound {r} = r & upper_bound {r} = r ) by Th22;
hence lower_bound {r} = upper_bound {r} ; :: thesis: verum