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