theorem :: MESFUN14:13

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