theorem Th6: :: INTEGRA1:8

for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for D being Division of A st i in dom D holds
divset (D,i) c= A