let A be non empty closed_interval Subset of REAL; :: thesis: for n being Nat st vol A > 0 & len (EqDiv (A,(2 |^ n))) = 1 holds

n = 0

let n be Nat; :: thesis: ( vol A > 0 & len (EqDiv (A,(2 |^ n))) = 1 implies n = 0 )

assume that

A1: vol A > 0 and

A2: len (EqDiv (A,(2 |^ n))) = 1 ; :: thesis: n = 0

2 |^ n > 0 by NEWTON:83;

then EqDiv (A,(2 |^ n)) divide_into_equal 2 |^ n by A1, Def1;

then len (EqDiv (A,(2 |^ n))) = 2 |^ n by INTEGRA4:def 1;

hence n = 0 by A2, NAT_1:14, NEWTON:86; :: thesis: verum

n = 0

let n be Nat; :: thesis: ( vol A > 0 & len (EqDiv (A,(2 |^ n))) = 1 implies n = 0 )

assume that

A1: vol A > 0 and

A2: len (EqDiv (A,(2 |^ n))) = 1 ; :: thesis: n = 0

2 |^ n > 0 by NEWTON:83;

then EqDiv (A,(2 |^ n)) divide_into_equal 2 |^ n by A1, Def1;

then len (EqDiv (A,(2 |^ n))) = 2 |^ n by INTEGRA4:def 1;

hence n = 0 by A2, NAT_1:14, NEWTON:86; :: thesis: verum