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