theorem :: RELSET_3:28

for q1, q2 being Rational holds (addRel (RAT,q1)) * (addRel (RAT,q2)) = addRel (RAT,(q1 + q2))