theorem :: RELSET_3:70

for n, n1, n2 being Nat
for X being natural-membered set holds
( [n1,n2] in multRel (X,n) iff ( n1 in X & n2 in X & n2 = n * n1 ) ) by Th42;