for I1, I2 being non empty closed_interval Subset of REAL
for jauge being positive-yielding Function of I1,REAL st I2 c= I1 holds
jauge | I2 is positive-yielding Function of I2,REAL by FUNCT_2:32;