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