theorem Th7: :: MSAFREE3:7

for S being non void Signature
for X being non-empty ManySortedSet of the carrier of S
for s being SortSymbol of S
for x being Term of S,X holds
( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s )