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