theorem :: RELSET_3:32

for i, i1, i2 being Integer
for X being integer-membered set holds
( [i1,i2] in addRel (X,i) iff ( i1 in X & i2 in X & i2 = i + i1 ) ) by Th11;