theorem Th8: :: MESFUN14:8

for a, b being Real
for A being non empty closed_interval Subset of REAL st a < b & A = [.a,b.] holds
for n being Nat st n > 0 holds
ex D being Division of A st D divide_into_equal n