set S = {{}};
set B = the BinOp of {{}};
take ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) ; :: thesis: ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is 1 -element
thus the carrier of ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is 1 -element ; :: according to STRUCT_0:def 19 :: thesis: verum