for I being non empty closed_interval Subset of REAL
for jauge being positive-yielding Function of I,REAL ex TD being tagged_division of I st TD is jauge -fine