let i, i1 be Integer; :: thesis: [i1,(i1 + i)] in addRel (INT,i)
( i1 in INT & i1 + i in INT ) by INT_1:def 2;
hence [i1,(i1 + i)] in addRel (INT,i) by Th11; :: thesis: verum