consider D being non empty set ;
consider l, r, i being BinOp of D;
take typealg(# D,l,r,i #) ; :: thesis: ( not typealg(# D,l,r,i #) is empty & typealg(# D,l,r,i #) is strict )
thus not the carrier of typealg(# D,l,r,i #) is empty ; :: according to STRUCT_0:def 1 :: thesis: typealg(# D,l,r,i #) is strict
thus typealg(# D,l,r,i #) is strict ; :: thesis: verum