theorem Th32: :: QUANTAL1:32

for Q being Girard-Quantale
for a being Element of Q holds
( a [*] (Top Q) = a & (Top Q) [*] a = a )