for a, b being Real
for jauge being positive-yielding Function of [.a,b.],REAL st a <= b holds
ex x being non empty increasing FinSequence of REAL ex t being non empty FinSequence of REAL st
( x . 1 = a & x . (len x) = b & t . 1 = a & dom x = dom t & ( for i being Nat st i - 1 in dom t & i in dom t holds
( (t . i) - (jauge . (t . i)) <= x . (i - 1) & x . (i - 1) <= t . i ) ) & ( for i being Nat st i in dom t holds
( t . i <= x . i & x . i <= (t . i) + (jauge . (t . i)) ) ) )