:: deftheorem defines Negation QUANTAL1:def 24 :
for G being non empty Girard-QuantaleStr
for b₂ being UnOp of G holds
( b₂ = Negation G iff for a being Element of G holds b₂ . a = Bottom a );