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 )

the absurd of Q is dualizing by Def20;

then A1: Top Q = the_unity_wrt H_{4}(Q)
by Th19;

H_{4}(Q) is having_a_unity
by MONOID_0:def 10;

hence ( a [*] (Top Q) = a & (Top Q) [*] a = a ) by A1, SETWISEO:15; :: thesis: verum

( a [*] (Top Q) = a & (Top Q) [*] a = a )

let a be Element of Q; :: thesis: ( a [*] (Top Q) = a & (Top Q) [*] a = a )

the absurd of Q is dualizing by Def20;

then A1: Top Q = the_unity_wrt H

H

hence ( a [*] (Top Q) = a & (Top Q) [*] a = a ) by A1, SETWISEO:15; :: thesis: verum