consider X being non empty set , a being BinOp of X, Z being Element of X, l being Function of [:the carrier of F,X:],X, r being Relation of X;
take SymStr(# X,a,Z,l,r #) ; :: thesis: not SymStr(# X,a,Z,l,r #) is empty
thus not the carrier of SymStr(# X,a,Z,l,r #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum