let S be locally_directed OrderSortedSign; for X being V2() 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 V2() 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 C be 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, y be object ; ( [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 ( 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)
;
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;
( 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;
verum
end;
given s1 being Element of S such that A6:
s1 in C
and
A7:
[x,s1] in (PTClasses X) . y
; [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; verum