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