consider l, r, i being BinOp of {{} }, d being Relation of ({{} } * ),{{} };
take typestr(# {{} },l,r,i,d #) ; :: thesis: ( not typestr(# {{} },l,r,i,d #) is empty & typestr(# {{} },l,r,i,d #) is strict )
thus not the carrier of typestr(# {{} },l,r,i,d #) is empty ; :: according to STRUCT_0:def 1 :: thesis: typestr(# {{} },l,r,i,d #) is strict
thus typestr(# {{} },l,r,i,d #) is strict ; :: thesis: verum