theorem :: RELSET_3:37

for n, n1, n2 being Nat
for X being natural-membered set holds
( [n1,n2] in addRel (X,n) iff ( n1 in X & n2 in X & n2 = n + n1 ) ) by Th11;