consider n, u being BinOp of (bool {} );
reconsider GG = LattStr(# (bool {} ),n,u #) 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

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
consider a being Element of GG;
take a ; :: thesis: a is_a_complement_of b
thus ( a "\/" b = Top GG & b "\/" a = Top GG ) by Lm1; :: according to LATTICES:def 18 :: thesis: ( a "/\" b = Bottom GG & b "/\" a = Bottom GG )
thus ( a "/\" b = Bottom GG & b "/\" a = Bottom GG ) by Lm1; :: thesis: verum

end;

thus GG is strict ; :: thesis: verum