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