theorem Th9: :: INTEGRA3:9

for A being non empty closed_interval Subset of REAL
for D being Division of A holds delta D >= 0