set l = the BinOp of {{}};
set d = the Relation of ({{}} *),{{}};
take
typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #)
; ( not typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) is empty & typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) is strict )
thus
not the carrier of typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) is empty
; STRUCT_0:def 1 typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) is strict
thus
typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) is strict
; verum