for I being non empty closed_interval Subset of REAL
for r being Real
for jauge being positive-yielding Function of I,REAL st jauge = r (#) (chi (I,I)) holds
0 < r