i1 - i2 = i1 + (- i2) ;
hence i1 - i2 is integer ; :: thesis: verum