consider X being non empty set , m, a being BinOp of X, M being Function of [:REAL,X:],X, u, Z being Element of X;
take AlgebraStr(# X,m,a,M,u,Z #) ; :: thesis: not AlgebraStr(# X,m,a,M,u,Z #) is empty
thus not the carrier of AlgebraStr(# X,m,a,M,u,Z #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum