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