let r be Real; :: thesis: vol {r} = 0
vol {r} = (upper_bound {r}) - (lower_bound {r}) by INTEGRA1:def 5
.= r - (lower_bound {r}) by Th36
.= r - r by Th36 ;
hence vol {r} = 0 ; :: thesis: verum