set u = the BinOp of (bool {});
take GG = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #); :: 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;
hence ( GG is strict & GG is Lattice-like ) ; :: thesis: verum