set B = BooleLatt {};
set e = the Element of (BooleLatt {});
set b = the BinOp of (BooleLatt {});
take Q = QuasiNetStr(# H₁( BooleLatt {}),H₂( BooleLatt {}),H₃( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #); :: 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: