let S be locally_directed OrderSortedSign; :: thesis: 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 ) )
let X be non-empty ManySortedSet of S; :: thesis: 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 ) )
let C be Component of S; :: thesis: 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 ) )
let x, y be object ; :: thesis: ( [x,y] in CompClass ((PTCongruence X),C) iff ex s1 being Element of S st
( s1 in C & [x,s1] in (PTClasses X) . y ) )

hereby :: thesis: ( ex s1 being Element of S st
( s1 in C & [x,s1] in (PTClasses X) . y ) implies [x,y] in CompClass ((PTCongruence X),C) )

assume [x,y] in CompClass ((PTCongruence X),C) ; :: thesis: ex s1 being Element of S st
( s1 in C & [x,s1] in (PTClasses X) . y )
then consider s1 being Element of S such that
A1: s1 in C and
A2: [x,y] in (PTCongruence X) . s1 by OSALG_4:def 9;
A3: [x,y] in { [x1,y1] where x1, y1 is Element of TS (DTConOSA X) : [x1,s1] in (PTClasses X) . y1 } by A2, Def22;
take s1 = s1; :: thesis: ( s1 in C & [x,s1] in (PTClasses X) . y )
consider x1, y1 being Element of TS (DTConOSA X) such that
A4: [x,y] = [x1,y1] and
A5: [x1,s1] in (PTClasses X) . y1 by A3;
x = x1 by A4, XTUPLE_0:1;
hence ( s1 in C & [x,s1] in (PTClasses X) . y ) by A1, A4, A5, XTUPLE_0:1; :: thesis: verum

end;

given s1 being Element of S such that A6: s1 in C and
A7: [x,s1] in (PTClasses X) . y ; :: thesis: [x,y] in CompClass ((PTCongruence X),C)
reconsider x2 = x, y2 = y as Element of TS (DTConOSA X) by A7, Th23;
[x2,y2] in { [x1,y1] where x1, y1 is Element of TS (DTConOSA X) : [x1,s1] in (PTClasses X) . y1 } by A7;
then [x2,y2] in (PTCongruence X) . s1 by Def22;
hence [x,y] in CompClass ((PTCongruence X),C) by A6, OSALG_4:def 9; :: thesis: verum