consider R being BinOp of {{} };
take TopGrStr(# {{} },R,(bool {{} }) #) ; :: thesis: ( TopGrStr(# {{} },R,(bool {{} }) #) is strict & TopGrStr(# {{} },R,(bool {{} }) #) is TopSpace-like & TopGrStr(# {{} },R,(bool {{} }) #) is trivial & not TopGrStr(# {{} },R,(bool {{} }) #) is empty )
1TopSp {{} } = TopStruct(# {{} },(bool {{} }) #) ;
hence ( TopGrStr(# {{} },R,(bool {{} }) #) is strict & TopGrStr(# {{} },R,(bool {{} }) #) is TopSpace-like & TopGrStr(# {{} },R,(bool {{} }) #) is trivial & not TopGrStr(# {{} },R,(bool {{} }) #) is empty ) by TEX_2:12; :: thesis: verum