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₄(Q) by Th19;
H₄(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