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