consider u, n being BinOp of (bool {} );
take GG = LattStr(# (bool {} ),u,n #); :: thesis: ( GG is strict & GG is Lattice-like )
A3: for x, y being Element of GG holds x "\/" y = y "\/" x by Lm1;
A4: for x, y, z being Element of GG holds x "\/" (y "\/" z) = (x "\/" y) "\/" z by Lm1;
A5: for x, y being Element of GG holds (x "/\" y) "\/" y = y by Lm1;
A6: for x, y being Element of GG holds x "/\" y = y "/\" x by Lm1;
A7: for x, y, z being Element of GG holds x "/\" (y "/\" z) = (x "/\" y) "/\" z by Lm1;
for x, y being Element of GG holds x "/\" (x "\/" y) = x 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 A3, A4, A5, A6, A7, Def4, Def5, Def6, Def7, Def8, Def9;
hence ( GG is strict & GG is Lattice-like ) ; :: thesis: verum