:: deftheorem defines multiplicative WAYBEL_7:def 7 :
for L being non empty RelStr
for R being Relation of the carrier of L holds
( R is multiplicative iff for a, x, y being Element of L st [a,x] in R & [a,y] in R holds
[a,(x "/\" y)] in R );