set A = {{}};
set B = the Element of {{}};
set C = the UnOp of {{}};
set D = the BinOp of {{}};
take NelsonStr(# {{}}, the Element of {{}}, the UnOp of {{}}, the UnOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) ; :: thesis: ( NelsonStr(# {{}}, the Element of {{}}, the UnOp of {{}}, the UnOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is strict & not NelsonStr(# {{}}, the Element of {{}}, the UnOp of {{}}, the UnOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is empty )
thus ( NelsonStr(# {{}}, the Element of {{}}, the UnOp of {{}}, the UnOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is strict & not NelsonStr(# {{}}, the Element of {{}}, the UnOp of {{}}, the UnOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is empty ) ; :: thesis: verum