:: deftheorem defines vol INTEGRA1:def 5 :
for A being Subset of REAL holds vol A = (upper_bound A) - (lower_bound A);