let n, u be BinOp of bool {} ; :: thesis: LattStr(# (bool {} ),n,u #) is 0_Lattice
set G = LattStr(# (bool {} ),n,u #);
reconsider G = LattStr(# (bool {} ),n,u #) as Lattice by Lm4;
reconsider D = {} as Element of by ZFMISC_1:def 1;
for x being Element of holds
( D "/\" x = D & x "/\" D = D ) ;
hence LattStr(# (bool {} ),n,u #) is 0_Lattice by Def13; :: thesis: verum