set L = {{},{{}}};
reconsider B = BooleLatt {{}} as non empty LattStr ;
bool {{}} = {{},{{}}}
by ZFMISC_1:24;
then A3:
the carrier of B = {{},{{}}}
by LATTICE3:def 1;
( {} in {{},{{}}} & {{}} in {{},{{}}} )
by TARSKI:def 2;
then
not B is trivial
by A3, ZFMISC_1:def 10;
hence
not for b1 being B_Lattice holds b1 is trivial
; verum