let A be closed-interval Subset of REAL ; :: thesis: for D2, MD2 being Division of A st MD2 = <*(lower_bound A)*> ^ D2 holds
vol (divset MD2,1) = 0
let D2, MD2 be Division of A; :: thesis: ( MD2 = <*(lower_bound A)*> ^ D2 implies vol (divset MD2,1) = 0 )
assume A1: MD2 = <*(lower_bound A)*> ^ D2 ; :: thesis: vol (divset MD2,1) = 0
rng MD2 <> {} ;
then 1 in dom MD2 by FINSEQ_3:34;
then ( lower_bound (divset MD2,1) = lower_bound A & upper_bound (divset MD2,1) = MD2 . 1 ) by INTEGRA1:def 5;
then vol (divset MD2,1) = (MD2 . 1) - (lower_bound A) by INTEGRA1:def 6
.= (lower_bound A) - (lower_bound A) by A1, FINSEQ_1:58 ;
hence vol (divset MD2,1) = 0 ; :: thesis: verum