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