:: deftheorem defines dualizing QUANTAL1:def 17 :
for Q being non empty QuantaleStr
for IT being Element of Q holds
( IT is dualizing iff for a being Element of Q holds
( (a -r> IT) -l> IT = a & (a -l> IT) -r> IT = a ) );