theorem :: RELSET_3:34

for i, i1 being Integer holds [i1,(i1 + i)] in addRel (INT,i)