:: deftheorem defines @ AOFA_L00:def 11 :
for J being non empty non void Signature
for X being empty-yielding ManySortedSet of the carrier of J
for Q being SubstMSAlgebra over J,X st X is ManySortedSubset of the Sorts of Q holds
for x being Element of Union X holds @ (x,Q) = x;