for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for jauge being positive-yielding Function of I,REAL
for r1, r2, s being Real
for D1 being Division of I
for fc, f being Function of I,REAL
for epsilon being Real st fc = chi (I,I) & r1 = min (rng (upper_volume (fc,D1))) & r2 = epsilon / ((2 * (len D1)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) & 0 < r1 & 0 < r2 & s = (min (r1,r2)) / 2 & jauge = s (#) fc & TD is jauge -fine holds
( delta (division_of TD) < min (rng (upper_volume (fc,D1))) & delta (division_of TD) < epsilon / ((2 * (len D1)) * |.((upper_bound (rng f)) - (lower_bound (rng f))).|) )