set l = the BinOp of {{}};
take typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) ; :: thesis: ( not typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is empty & typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is strict )
thus not the carrier of typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is empty ; :: according to STRUCT_0:def 1 :: thesis: typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is strict
thus typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is strict ; :: thesis: verum