let a be Real; :: thesis: for A being Subset of REAL
for rho being real-valued Function st A c= [.a,a.] holds
vol (A,rho) = 0
let A be Subset of REAL; :: thesis: for rho being real-valued Function st A c= [.a,a.] holds
vol (A,rho) = 0
let rho be real-valued Function; :: thesis: ( A c= [.a,a.] implies vol (A,rho) = 0 )
assume A c= [.a,a.] ; :: thesis: vol (A,rho) = 0
then A c= {a} by XXREAL_1:17;
per cases then ( A = {} or A = {a} ) by ZFMISC_1:33;
suppose A = {} ; :: thesis: vol (A,rho) = 0
hence vol (A,rho) = 0 by INTEGR22:def 1; :: thesis: verum
end;
suppose A = {a} ; :: thesis: vol (A,rho) = 0
hence vol (A,rho) = (rho . (upper_bound {a})) - (rho . (lower_bound {a})) by INTEGR22:def 1
.= (rho . (upper_bound {a})) - (rho . (upper_bound {a})) by SEQ_4:10
.= 0 ;
:: thesis: verum
end;
end;