let n, u be BinOp of (bool {}); :: thesis: LattStr(# (bool {}),n,u #) is Lattice
set G = LattStr(# (bool {}),n,u #);
for x, y, z being Element of LattStr(# (bool {}),n,u #) holds x "\/" (y "\/" z) = (x "\/" y) "\/" z by Lm1;
then A1: LattStr(# (bool {}),n,u #) is join-associative ;
for x, y being Element of LattStr(# (bool {}),n,u #) holds (x "/\" y) "\/" y = y by Lm1;
then A2: LattStr(# (bool {}),n,u #) is meet-absorbing ;
for x, y being Element of LattStr(# (bool {}),n,u #) holds x "/\" (x "\/" y) = x by Lm1;
then A3: LattStr(# (bool {}),n,u #) is join-absorbing ;
for x, y, z being Element of LattStr(# (bool {}),n,u #) holds x "/\" (y "/\" z) = (x "/\" y) "/\" z by Lm1;
then A4: LattStr(# (bool {}),n,u #) is meet-associative ;
for x, y being Element of LattStr(# (bool {}),n,u #) holds x "/\" y = y "/\" x by Lm1;
then A5: LattStr(# (bool {}),n,u #) is meet-commutative ;
for x, y being Element of LattStr(# (bool {}),n,u #) holds x "\/" y = y "\/" x by Lm1;
then LattStr(# (bool {}),n,u #) is join-commutative ;
hence LattStr(# (bool {}),n,u #) is Lattice by A1, A2, A5, A4, A3; :: thesis: verum