let q, q1 be Rational; :: thesis: [q1,(q1 + q)] in addRel (RAT,q)
( q1 in RAT & q1 + q in RAT ) by RAT_1:def 2;
hence [q1,(q1 + q)] in addRel (RAT,q) by Th11; :: thesis: verum