set X = the non empty set ;
set m = the BinOp of the non empty set ;
set M = the Function of [:REAL, the non empty set :], the non empty set ;
set u = the Element of the non empty set ;
take
AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #)
; not AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty
thus
not the carrier of AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set #) is empty
; STRUCT_0:def 1 verum