theorem Th28: :: OSAFREE:28

for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for s being Element of S holds PTVars (s,X) = { (root-tree t) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) }