for x being set
for S being non void Signature
for X being V8() ManySortedSet of the carrier of S holds
( x is Element of (FreeMSA X) iff x is Term of S,X )