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

end;

given s1 being Element of S such that A4: ( s1 in C & [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 A4, Th24;
[x2,y2] in { [x1,y1] where x1, y1 is Element of TS (DTConOSA X) : [x1,s1] in (PTClasses X) . y1 } by A4;
then [x2,y2] in (PTCongruence X) . s1 by Def23;
hence [x,y] in CompClass (PTCongruence X),C by A4, OSALG_4:def 11; :: thesis: verum