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

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