theorem :: RELSET_3:30

for q being Rational holds addRel (RAT,q) = { [q1,(q1 + q)] where q1 is Rational : verum }