- t2 is INT-Expression of A,f ;
hence t1 - t2 is INT-Expression of A,f by Def22; :: thesis: verum