theorem :: RELSET_3:55

for r, r1, r2 being Real
for X being real-membered set holds
( [r1,r2] in multRel (X,r) iff ( r1 in X & r2 in X & r2 = r * r1 ) ) by Th42;