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