set B = BooleLatt {};
consider b being BinOp of (BooleLatt {});
consider e being Element of (BooleLatt {});
take Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) ; :: thesis: ( Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is associative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is commutative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is unital & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is left-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is right-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is complete & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is Lattice-like & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is cyclic & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is dualized & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is strict )
thus ( Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is associative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is commutative & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is unital & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is left-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is right-distributive & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is complete & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is Lattice-like & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is cyclic & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is dualized & Girard-QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}),b,e,e #) is strict ) by Th4, Th21; :: thesis: verum