let S be locally_directed OrderSortedSign; :: thesis: for X being V5() ManySortedSet of S
for C being Component of S
for x, y being set 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 V5() ManySortedSet of S; :: thesis: for C being Component of S
for x, y being set 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 set 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 set ; :: 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 11;
A3: [x,y] in { [x1,y1] where x1, y1 is Element of TS (DTConOSA X) : [x1,s1] in (PTClasses X) . y1 } by A2, Def23;
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, ZFMISC_1:33;
hence ( s1 in C & [x,s1] in (PTClasses X) . y ) by A1, A4, A5, ZFMISC_1:33; :: 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, Th24;
[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 Def23;
hence [x,y] in CompClass (PTCongruence X),C by A6, OSALG_4:def 11; :: thesis: verum