let q, q1 be Rational; :: thesis: [q1,(q1 * q)] in multRel (RAT,q)
( q1 in RAT & q1 * q in RAT ) by RAT_1:def 2;
hence [q1,(q1 * q)] in multRel (RAT,q) by Th42; :: thesis: verum