set u = the BinOp of (bool {});
take L = /\-SemiLattStr(# (bool {}), the BinOp of (bool {}) #); :: thesis: ( L is 1 -element & L is strict )
the carrier of L = {{}} by ZFMISC_1:1;
then the carrier of L is 1 -element ;
hence ( L is 1 -element & L is strict ) by STRUCT_0:def 19; :: thesis: verum