let A be non empty 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 A2: 1 in dom MD2 by FINSEQ_3:32;
then A3: upper_bound (divset (MD2,1)) = MD2 . 1 by INTEGRA1:def 4;
lower_bound (divset (MD2,1)) = lower_bound A by A2, INTEGRA1:def 4;
then vol (divset (MD2,1)) = (MD2 . 1) - (lower_bound A) by A3, INTEGRA1:def 5
.= (lower_bound A) - (lower_bound A) by A1, FINSEQ_1:41 ;
hence vol (divset (MD2,1)) = 0 ; :: thesis: verum