:: deftheorem Def2 defines xvol INTEGR20:def 2 :
for A being Subset of REAL holds
( ( A is empty implies xvol A = 0 ) & ( not A is empty implies xvol A = vol A ) );