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 SEQ_4:9
.= r - r by SEQ_4:9 ;
hence vol {r} = 0 ; :: thesis: verum