set B = BooleLatt {};
consider e being Element of (BooleLatt {}), b being BinOp of (BooleLatt {});
take QuasiNetStr(# H₁( BooleLatt {}),H₂( BooleLatt {}),H₃( BooleLatt {}),b,e #) ; :: thesis: ( QuasiNetStr(# H₁( BooleLatt {}),H₂( BooleLatt {}),H₃( BooleLatt {}),b,e #) is complete & QuasiNetStr(# H₁( BooleLatt {}),H₂( BooleLatt {}),H₃( BooleLatt {}),b,e #) is Lattice-like )
thus ( QuasiNetStr(# H₁( BooleLatt {}),H₂( BooleLatt {}),H₃( BooleLatt {}),b,e #) is complete & QuasiNetStr(# H₁( BooleLatt {}),H₂( BooleLatt {}),H₃( BooleLatt {}),b,e #) is Lattice-like ) by Th4; :: thesis: verum