consider u, n being BinOp of (bool {} );
take GG = LattStr(# (bool {} ),u,n #); :: thesis: ( GG is strict & GG is Lattice-like )
A1: ( ( for x, y being Element of GG holds (x "/\" y) "\/" y = y ) & ( for x, y being Element of GG holds x "/\" y = y "/\" x ) ) by Lm1;
A2: ( ( for x, y, z being Element of GG holds x "/\" (y "/\" z) = (x "/\" y) "/\" z ) & ( for x, y being Element of GG holds x "/\" (x "\/" y) = x ) ) by Lm1;
( ( for x, y being Element of GG holds x "\/" y = y "\/" x ) & ( for x, y, z being Element of GG holds x "\/" (y "\/" z) = (x "\/" y) "\/" z ) ) by Lm1;
then ( GG is join-commutative & GG is join-associative & GG is meet-absorbing & GG is meet-commutative & GG is meet-associative & GG is join-absorbing ) by A1, A2, Def4, Def5, Def6, Def7, Def8, Def9;
hence ( GG is strict & GG is Lattice-like ) ; :: thesis: verum