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