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