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