theorem Th24: :: OSAFREE:24

for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for C being Component of S
for x, y being object holds
( [x,y] in CompClass ((PTCongruence X),C) iff ex s1 being Element of S st
( s1 in C & [x,s1] in (PTClasses X) . y ) )