set A = the non trivial set ;
take ConjNormAlgStr(# the non trivial set , the BinOp of the non trivial set , the BinOp of the non trivial set , the Function of [:REAL, the non trivial set :], the non trivial set , the Element of the non trivial set , the Element of the non trivial set , the Function of the non trivial set ,REAL, the Function of the non trivial set , the non trivial set #) ; :: thesis: ( not ConjNormAlgStr(# the non trivial set , the BinOp of the non trivial set , the BinOp of the non trivial set , the Function of [:REAL, the non trivial set :], the non trivial set , the Element of the non trivial set , the Element of the non trivial set , the Function of the non trivial set ,REAL, the Function of the non trivial set , the non trivial set #) is trivial & ConjNormAlgStr(# the non trivial set , the BinOp of the non trivial set , the BinOp of the non trivial set , the Function of [:REAL, the non trivial set :], the non trivial set , the Element of the non trivial set , the Element of the non trivial set , the Function of the non trivial set ,REAL, the Function of the non trivial set , the non trivial set #) is strict )
thus ( not ConjNormAlgStr(# the non trivial set , the BinOp of the non trivial set , the BinOp of the non trivial set , the Function of [:REAL, the non trivial set :], the non trivial set , the Element of the non trivial set , the Element of the non trivial set , the Function of the non trivial set ,REAL, the Function of the non trivial set , the non trivial set #) is trivial & ConjNormAlgStr(# the non trivial set , the BinOp of the non trivial set , the BinOp of the non trivial set , the Function of [:REAL, the non trivial set :], the non trivial set , the Element of the non trivial set , the Element of the non trivial set , the Function of the non trivial set ,REAL, the Function of the non trivial set , the non trivial set #) is strict ) ; :: thesis: verum