let n, u be BinOp of (bool {}); :: thesis: LattStr(# (bool {}),n,u #) is 1_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 1_Lattice by Def14; :: thesis: verum