set R = the BinOp of {{}};
take TopaddGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) ; :: thesis: ( TopaddGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is strict & TopaddGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is TopSpace-like & TopaddGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is 1 -element )
the carrier of (1TopSp {{}}) is 1 -element ;
hence ( TopaddGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is strict & TopaddGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is TopSpace-like & TopaddGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is 1 -element ) by TEX_2:7; :: thesis: verum