:: deftheorem Defvol defines vol INTEGR22:def 1 :
for A being Subset of REAL
for rho being real-valued Function holds
( ( A is empty implies vol (A,rho) = 0 ) & ( not A is empty implies vol (A,rho) = (rho . (upper_bound A)) - (rho . (lower_bound A)) ) );