theorem Th12: :: OSAFREE:12

for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
( nt in NonTerminals (DTConOSA X) & nt -tree ts in TS (DTConOSA X) & ex o being OperSymbol of S st
( nt = [o, the carrier of S] & ts in Args (o,(ParsedTermsOSA X)) & nt -tree ts = (Den (o,(ParsedTermsOSA X))) . ts & ( for s1 being Element of S holds
( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) ) )