theorem Th11: :: OSAFREE:11

for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for t being Element of TS (DTConOSA X)
for o being OperSymbol of S st t . {} = [o, the carrier of S] holds
( ex p being SubtreeSeq of OSSym (o,X) st
( t = (OSSym (o,X)) -tree p & OSSym (o,X) ==> roots p & p in Args (o,(ParsedTermsOSA X)) & t = (Den (o,(ParsedTermsOSA X))) . p ) & ( for s2 being Element of S
for x being set holds t <> root-tree [x,s2] ) & ( for s1 being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) )