theorem :: RELSET_3:60

for q, q1, q2 being Rational
for X being rational-membered set holds
( [q1,q2] in multRel (X,q) iff ( q1 in X & q2 in X & q2 = q * q1 ) ) by Th42;