consider uu, nn being BinOp of (bool {} );
set G = LattStr(# (bool {} ),uu,nn #);
reconsider G = LattStr(# (bool {} ),uu,nn #) as Lattice by Lm4;
( G is 0_Lattice & G is 1_Lattice ) by Lm5, Lm6;
then G is bounded ;
hence ex b₁ being Lattice st
( b₁ is bounded & b₁ is strict ) ; :: thesis: verum