set ZS = the non empty set ;
set O = the Element of the non empty set ;
set F = the BinOp of the non empty set ;
set G = the Function of [:INT, the non empty set :], the non empty set ;
take Z_ModuleStruct(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:INT, the non empty set :], the non empty set #) ; :: thesis: not Z_ModuleStruct(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:INT, the non empty set :], the non empty set #) is empty
thus not the carrier of Z_ModuleStruct(# the non empty set , the Element of the non empty set , the BinOp of the non empty set , the Function of [:INT, the non empty set :], the non empty set #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum