set A = the non empty set ;
set b1 = the BinOp of the non empty set ;
take QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set #) ; :: thesis: not QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set #) is empty
thus not the carrier of QuantaleStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the BinOp of the non empty set #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum