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