theorem Th18: :: MSAFREE3:18

for x being set
for S being non void Signature
for Y being non-empty ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )