let I be non empty closed_interval Subset of REAL; :: thesis: ( not I is empty & I is trivial implies vol I = 0 )
assume ( not I is empty & I is trivial ) ; :: thesis: vol I = 0
then consider x being object such that
A1: I = {x} by ZFMISC_1:131;
x in I by A1, TARSKI:def 1;
then reconsider x = x as Real ;
vol {x} = 0 by COUSIN:41;
hence vol I = 0 by A1; :: thesis: verum