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