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