theorem :: RELSET_3:65

for i, i1, i2 being Integer
for X being integer-membered set holds
( [i1,i2] in multRel (X,i) iff ( i1 in X & i2 in X & i2 = i * i1 ) ) by Th42;