theorem :: MESFUN14:14

for a, b being Real
for A being non empty closed_interval Subset of REAL st a < b & A = [.a,b.] holds
ex D being DivSequence of A st
for n being Nat holds D . n divide_into_equal 2 |^ n