consider uu, nn being BinOp of (bool {} );
set GG = LattStr(# (bool {} ),uu,nn #);
reconsider GG = LattStr(# (bool {} ),uu,nn #) as Lattice by Lm4;
for x, y, z being Element of GG st x [= z holds
x "\/" (y "/\" z) = (x "\/" y) "/\" z by Lm1;
then A1: GG is modular by Def12;
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 A2: GG is lower-bounded by Def13;
A3: for x, y, z being Element of GG holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by Lm1;
A4: for x being Element of GG holds
( D "\/" x = D & x "\/" D = D ) ;
A5: GG is distributive by A3, Def11;
GG is upper-bounded by A4, Def14;
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, A2, A5; :: thesis: verum