theorem Th9: :: QUANTAL1:9

for Q being Quantale
for a, b, c, d being Element of Q st a [= b & c [= d holds
a [*] c [= b [*] d