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