:: deftheorem defines delta QUANTAL1:def 27 :
for Q being Girard-Quantale
for a, b being Element of Q holds a delta b = Bottom ((Bottom a) [*] (Bottom b));