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