:: deftheorem Def23 defines PTVars OSAFREE:def 23 :
for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for s being Element of S
for b₄ being Subset of ( the Sorts of (ParsedTermsOSA X) . s) holds
( b₄ = PTVars (s,X) iff for x being object holds
( x in b₄ iff ex a being object st
( a in X . s & x = root-tree [a,s] ) ) );