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