theorem Th20: :: MSAFREE3:20

for S being non void Signature
for X being non-empty ManySortedSet of the carrier of S
for A being MSSubset of (FreeMSA X) holds
( A is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds
(Sym (o,X)) -tree p in A . (the_result_sort_of o) )