:: deftheorem defines Bottom QUANTAL1:def 25 :
for G being non empty Girard-QuantaleStr
for u being UnOp of G holds Bottom u = (Negation G) * u;