set S = {{}};
set B = the BinOp of {{}};
take ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) ; :: thesis: not ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is empty
thus not ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is empty by STRUCT_0:def 1; :: thesis: verum