theorem Th18: :: OSAFREE:18

for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for o being OperSymbol of S
for x being FinSequence of TS (DTConOSA X) holds
( LeastSorts x <= the_arity_of o iff x in Args (o,(ParsedTermsOSA X)) )