theorem Th12: :: INTEGR20:12

for A being non empty closed_interval Subset of REAL
for D being Division of A
for r being Real st delta D < r holds
for i being Nat
for s, t being Real st i in dom D & s in divset (D,i) & t in divset (D,i) holds
|.(s - t).| < r