for I being non empty closed_interval Subset of REAL
for jauge1, jauge2 being positive-yielding Function of I,REAL
for TD being b₂ -fine tagged_division of I st jauge1 <= jauge2 holds
TD is b₃ -fine tagged_division of I