set n = the BinOp of (bool {});
reconsider G = LattStr(# (bool {}), the BinOp of (bool {}), the BinOp of (bool {}) #) as strict Lattice by Lm4;
A1: G is complemented
proof
let b be Element of G; :: according to LATTICES:def 19 :: thesis: ex a being Element of G st a is_a_complement_of b
take b ; :: thesis: b is_a_complement_of b
thus ( b "\/" b = Top G & b "\/" b = Top G ) by Lm1; :: according to LATTICES:def 18 :: thesis: ( b "/\" b = Bottom G & b "/\" b = Bottom G )
thus ( b "/\" b = Bottom G & b "/\" b = Bottom G ) by Lm1; :: thesis: verum
end;
( G is 0_Lattice & G is 1_Lattice ) by Lm5, Lm6;
then reconsider G = G as C_Lattice by A1;
for x, y, z being Element of G holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by Lm1;
then G is distributive ;
hence ex b1 being Lattice st
( b1 is Boolean & b1 is strict ) ; :: thesis: verum