theorem :: RELSET_3:27

for q, q1, q2 being Rational
for X being rational-membered set holds
( [q1,q2] in addRel (X,q) iff ( q1 in X & q2 in X & q2 = q + q1 ) ) by Th11;