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