let r be Real; :: thesis: ( upper_bound {r} = r & lower_bound {r} = r )
thus upper_bound {r} = upper_bound [.r,r.] by XXREAL_1:17
.= r by JORDAN5A:19 ; :: thesis: lower_bound {r} = r
thus lower_bound {r} = lower_bound [.r,r.] by XXREAL_1:17
.= r by JORDAN5A:19 ; :: thesis: verum