begin
Lm1:
for uu, nn being BinOp of (bool {})
for x, y being Element of LattStr(# (bool {}),uu,nn #) holds x = y
Lm2:
for n being BinOp of (bool {})
for x, y being Element of \/-SemiLattStr(# (bool {}),n #) holds x = y
Lm3:
for n being BinOp of (bool {})
for x, y being Element of /\-SemiLattStr(# (bool {}),n #) holds x = y
Lm4:
for n, u being BinOp of (bool {}) holds LattStr(# (bool {}),n,u #) is Lattice
Lm5:
for n, u being BinOp of (bool {}) holds LattStr(# (bool {}),n,u #) is 0_Lattice
Lm6:
for n, u being BinOp of (bool {}) holds LattStr(# (bool {}),n,u #) is 1_Lattice
begin