theorem Th30: :: MSAFREE3:30

for S being non void Signature
for X, Y being non-empty ManySortedSet of the carrier of S
for t being Term of S,Y st variables_in t c= X holds
t is Term of S,X