thus t1 - t2 is Function of X,INT ; :: thesis: verum