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 holds x "\/" (y "\/" z) = (x "\/" y) "\/" z by Lm1;
then A1: LattStr(# (bool {} ),n,u #) is join-associative by Def5;
for x, y being Element of holds (x "/\" y) "\/" y = y by Lm1;
then A2: LattStr(# (bool {} ),n,u #) is meet-absorbing by Def8;
for x, y being Element of holds x "/\" (x "\/" y) = x by Lm1;
then A3: LattStr(# (bool {} ),n,u #) is join-absorbing by Def9;
for x, y, z being Element of holds x "/\" (y "/\" z) = (x "/\" y) "/\" z by Lm1;
then A4: LattStr(# (bool {} ),n,u #) is meet-associative by Def7;
for x, y being Element of holds x "/\" y = y "/\" x by Lm1;
then A5: LattStr(# (bool {} ),n,u #) is meet-commutative by Def6;
for x, y being Element of holds x "\/" y = y "\/" x by Lm1;
then LattStr(# (bool {} ),n,u #) is join-commutative by Def4;
hence LattStr(# (bool {} ),n,u #) is Lattice by A1, A2, A5, A4, A3; :: thesis: verum