:: deftheorem defines Bottom QUANTAL1:def 26 :
for G being non empty Girard-QuantaleStr
for o being BinOp of G holds Bottom o = (Negation G) * o;