set uu = the BinOp of (bool {});
set GG = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #);
reconsider GG = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #) as Lattice by Lm4;
reconsider 0GG = {} , D = {} as Element of GG by ZFMISC_1:def 1;
for x being Element of GG holds
( 0GG "/\" x = 0GG & x "/\" 0GG = 0GG ) ;
then A1: GG is lower-bounded ;
for x being Element of GG holds
( D "\/" x = D & x "\/" D = D ) ;
then A2: GG is upper-bounded ;
for x, y, z being Element of GG holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by Lm1;
then A3: GG is distributive ;
for x, y, z being Element of GG st x [= z holds
x "\/" (y "/\" z) = (x "\/" y) "/\" z by Lm1;
then GG is modular ;
hence ex b₁ being Lattice st
( b₁ is strict & b₁ is distributive & b₁ is lower-bounded & b₁ is upper-bounded & b₁ is modular ) by A1, A3, A2; :: thesis: verum