:: deftheorem Def15 defines FreeGen MSAFREE:def 15 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for s being SortSymbol of S
for b₄ being Subset of ((FreeSort X) . s) holds
( b₄ = FreeGen (s,X) iff for x being set holds
( x in b₄ iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) );