theorem Th12: :: QUANTAL1:12

for Q being Quantale
for a, b, c being Element of Q holds
( a [*] b [= c iff a [= b -r> c )