theorem Th22: :: MSAFREE3:22

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 holds (Reverse Y) "" X c= S -Terms (X,Y)