set R = the BinOp of {{}};
set T = the Subset-Family of {{}};
take TopaddGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) ; :: thesis: ( TopaddGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is strict & not TopaddGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is empty )
thus ( TopaddGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is strict & not TopaddGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is empty ) ; :: thesis: verum