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