for S being locally_directed OrderSortedSign
for X being V2() ManySortedSet of S
for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s holds OSClass ((PTCongruence X),x) = proj1 ((PTClasses X) . x)