set B = BooleLatt {};
consider e being Element of (BooleLatt {}), b being BinOp of (BooleLatt {});
take Q = QuasiNetStr(# H₁( BooleLatt {}),H₂( BooleLatt {}),H₃( BooleLatt {}),b,e #); :: thesis:
( Q is with_zero & Q is unital ) by Th4;
hence ( Q is associative & Q is commutative & Q is unital & Q is with_zero & Q is with_left-zero & Q is left-distributive & Q is right-distributive & Q is complete & Q is Lattice-like ) by Th4; :: thesis: