theorem Th11: :: QUANTAL1:11

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