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 G by ZFMISC_1:def 1;
for x being Element of G holds
( D "/\" x = D & x "/\" D = D ) ;
hence LattStr(# (bool {}),n,u #) is 0_Lattice by Def13; :: thesis: verum