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