theorem Th15: :: INTEGRA6:15

for A being non empty closed_interval Subset of REAL
for n being Nat st n > 0 & vol A > 0 holds
ex D being Division of A st
( len D = n & ( for i being Nat st i in dom D holds
D . i = (lower_bound A) + (((vol A) / n) * i) ) )