theorem Th21: :: OSAFREE:21

for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for x, y being Element of TS (DTConOSA X)
for s1, s2 being Element of S st s1 <= s2 & x in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 holds
( [y,s1] in (PTClasses X) . x iff [y,s2] in (PTClasses X) . x )