set B = BooleLatt {};
set b = the BinOp of (BooleLatt {});
take
QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #)
; ( QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is associative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is commutative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is unital & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is with_zero & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is left-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is right-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is complete & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is Lattice-like )
thus
( QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is associative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is commutative & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is unital & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is with_zero & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is left-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is right-distributive & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is complete & QuantaleStr(# H1( BooleLatt {}),H2( BooleLatt {}),H3( BooleLatt {}), the BinOp of (BooleLatt {}) #) is Lattice-like )
by Th4; verum