:: deftheorem Def24 defines PTVars OSAFREE:def 24 :
for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for b₃ being MSSubset of (ParsedTermsOSA X) holds
( b₃ = PTVars X iff for s being Element of S holds b₃ . s = PTVars (s,X) );