:: deftheorem Def20 defines dualized QUANTAL1:def 20 :
for IT being non empty Girard-QuantaleStr holds
( IT is dualized iff the absurd of IT is dualizing );