set l = the BinOp of {{}};
set d = the Relation of ({{}} *),{{}};
take typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) ; :: thesis: ( 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 ; :: according to STRUCT_0:def 1 :: thesis: 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 ; :: thesis: verum