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