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 ZFMISC_1:1; :: thesis: verum