let Q be Girard-Quantale; :: thesis: for a being Element of Q holds
( a [*] (Top Q) = a & (Top Q) [*] a = a )
let a be Element of Q; :: thesis: ( a [*] (Top Q) = a & (Top Q) [*] a = a )
( Top Q = (Bottom Q) -r> (Bottom Q) & Bottom Q = the absurd of Q & the absurd of Q is dualizing ) by Def20;
then ( Top Q = the_unity_wrt H₄(Q) & H₄(Q) is having_a_unity ) by Th19, MONOID_0:def 10;
hence ( a [*] (Top Q) = a & (Top Q) [*] a = a ) by SETWISEO:23; :: thesis: verum