theorem Th19: :: QUANTAL1:19
for Q being Quantale
for D being Element of Q st D is dualizing holds
( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )