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