for I being non empty closed_interval Subset of REAL
for r being Real
for jauge being positive-yielding Function of I,REAL
for D being tagged_division of I st jauge = r (#) (chi (I,I)) & D is jauge -fine holds
delta (division_of D) <= r