:: deftheorem Def22 defines PTCongruence OSAFREE:def 22 :
for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for b₃ being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X holds
( b₃ = PTCongruence X iff for i being set st i in the carrier of S holds
b₃ . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } );