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 1 -element )
the carrier of (1TopSp {{}}) is 1 -element ;
hence ( TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is strict & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is TopSpace-like & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is 1 -element ) by TEX_2:7; :: thesis: verum