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