consider A being non empty set , m being BinOp of A;
take BCIStr(# A,m #) ; :: thesis: ( not BCIStr(# A,m #) is empty & BCIStr(# A,m #) is strict )
thus not the carrier of BCIStr(# A,m #) is empty ; :: according to STRUCT_0:def 1 :: thesis: BCIStr(# A,m #) is strict
thus BCIStr(# A,m #) is strict ; :: thesis: verum