set B = BooleLatt {};

set e = the Element of (BooleLatt {});

set b = the BinOp of (BooleLatt {});

take Q = QuasiNetStr(# H_{1}( BooleLatt {}),H_{2}( BooleLatt {}),H_{3}( BooleLatt {}), the BinOp of (BooleLatt {}), the Element of (BooleLatt {}) #); :: thesis: ( 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 )

( 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: verum

set e = the Element of (BooleLatt {});

set b = the BinOp of (BooleLatt {});

take Q = QuasiNetStr(# H

( 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: verum