defpred S₁[ object , object ] means ex s1 being Element of S st
( s1 in C & [$1,$2] in E . s1 );
A1: E is os-compatible by Def2;

per cases ;

suppose A2: the Sorts of A -carrier_of C is empty ; :: thesis:

for x, y being object holds
( [x,y] in {} iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )

proof

let x, y be object ; :: thesis:
thus ( [x,y] in {} implies ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ; :: thesis:
assume ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ; :: thesis:
then consider s1 being Element of S such that
A3: ( s1 in C & [x,y] in E . s1 ) ;
( x in the Sorts of A . s1 & the Sorts of A . s1 in { ( the Sorts of A . s) where s is Element of S : s in C } ) by A3, ZFMISC_1:87;
hence [x,y] in {} by A2, TARSKI:def 4; :: thesis:

end;

hence ex b₁ being Equivalence_Relation of ( the Sorts of A -carrier_of C) st
for x, y being object holds
( [x,y] in b₁ iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) by A2, Th9; :: thesis:

end;

suppose not the Sorts of A -carrier_of C is empty ; :: thesis:

then reconsider SAC = the Sorts of A -carrier_of C as non empty set ;
set CC = { [x,y] where x, y is Element of SAC : S₁[x,y] } ;
{ [x,y] where x, y is Element of SAC : S₁[x,y] } c= [:SAC,SAC:]

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { [x,y] where x, y is Element of SAC : S₁[x,y] } ; :: thesis:
then ex x, y being Element of SAC st
( z = [x,y] & S₁[x,y] ) ;
hence z in [:SAC,SAC:] by ZFMISC_1:87; :: thesis:

end;

then reconsider P1 = { [x,y] where x, y is Element of SAC : S₁[x,y] } as Relation of SAC ;

now :: thesis:

let x, y be object ; :: thesis:
assume that
A4: ( x in SAC & y in SAC ) and
A5: [x,y] in P1 ; :: thesis:
reconsider x1 = x, y1 = y as Element of SAC by A4;
consider x2, y2 being Element of SAC such that
A6: [x,y] = [x2,y2] and
A7: S₁[x2,y2] by A5;
A8: ( x = x2 & y = y2 ) by A6, XTUPLE_0:1;
consider s5 being Element of S such that
A9: s5 in C and
A10: [x2,y2] in E . s5 by A7;
field (E . s5) = the Sorts of A . s5 by ORDERS_1:12;
then A11: E . s5 is_symmetric_in the Sorts of A . s5 by RELAT_2:def 11;
( x2 in the Sorts of A . s5 & y2 in the Sorts of A . s5 ) by A10, ZFMISC_1:87;
then [y,x] in E . s5 by A8, A10, A11, RELAT_2:def 3;
then [y1,x1] in { [x,y] where x, y is Element of SAC : S₁[x,y] } by A9;
hence [y,x] in P1 ; :: thesis:

end;

then A12: P1 is_symmetric_in SAC by RELAT_2:def 3;

now :: thesis:

let x be object ; :: thesis:
assume A13: x in SAC ; :: thesis:
reconsider x1 = x as Element of SAC by A13;
consider X being set such that
A14: x in X and
A15: X in { ( the Sorts of A . s) where s is Element of S : s in C } by A13, TARSKI:def 4;
consider s being Element of S such that
A16: X = the Sorts of A . s and
A17: s in C by A15;
field (E . s) = the Sorts of A . s by ORDERS_1:12;
then E . s is_reflexive_in the Sorts of A . s by RELAT_2:def 9;
then [x,x] in E . s by A14, A16, RELAT_2:def 1;
then [x1,x1] in { [x,y] where x, y is Element of SAC : S₁[x,y] } by A17;
hence [x,x] in P1 ; :: thesis:

end;

then P1 is_reflexive_in SAC by RELAT_2:def 1;
then A18: ( dom P1 = SAC & field P1 = SAC ) by ORDERS_1:13;

now :: thesis:

let x, y, z be object ; :: thesis:
assume that
x in SAC and
y in SAC and
z in SAC and
A19: [x,y] in P1 and
A20: [y,z] in P1 ; :: thesis:
consider x2, y2 being Element of SAC such that
A21: [x,y] = [x2,y2] and
A22: S₁[x2,y2] by A19;
A23: x = x2 by A21, XTUPLE_0:1;
consider y3, z3 being Element of SAC such that
A24: [y,z] = [y3,z3] and
A25: S₁[y3,z3] by A20;
A26: y = y3 by A24, XTUPLE_0:1;
consider s5 being Element of S such that
A27: s5 in C and
A28: [x2,y2] in E . s5 by A22;
consider s6 being Element of S such that
A29: s6 in C and
A30: [y3,z3] in E . s6 by A25;
reconsider s51 = s5, s61 = s6 as Element of S ;
consider su being Element of S such that
A31: su in C and
A32: s51 <= su and
A33: s61 <= su by A27, A29, WAYBEL_0:def 1;
( y3 in the Sorts of A . s6 & z3 in the Sorts of A . s6 ) by A30, ZFMISC_1:87;
then A34: [y3,z3] in E . su by A1, A30, A33;
then A35: z3 in the Sorts of A . su by ZFMISC_1:87;
A36: z = z3 by A24, XTUPLE_0:1;
A37: y = y2 by A21, XTUPLE_0:1;
field (E . su) = the Sorts of A . su by ORDERS_1:12;
then A38: E . su is_transitive_in the Sorts of A . su by RELAT_2:def 16;
( x2 in the Sorts of A . s5 & y2 in the Sorts of A . s5 ) by A28, ZFMISC_1:87;
then A39: [x2,y2] in E . su by A1, A28, A32;
then ( x2 in the Sorts of A . su & y2 in the Sorts of A . su ) by ZFMISC_1:87;
then [x2,z3] in E . su by A37, A26, A39, A34, A35, A38, RELAT_2:def 8;
hence [x,z] in P1 by A23, A36, A31; :: thesis:

end;

then P1 is_transitive_in SAC by RELAT_2:def 8;
then reconsider P1 = P1 as Equivalence_Relation of ( the Sorts of A -carrier_of C) by A18, A12, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
take P1 ; :: thesis:
for x, y being object holds
( [x,y] in { [x,y] where x, y is Element of SAC : S₁[x,y] } iff S₁[x,y] )

proof

let x, y be object ; :: thesis:

hereby :: thesis:

assume [x,y] in { [x,y] where x, y is Element of SAC : S₁[x,y] } ; :: thesis:
then ex x1, y1 being Element of SAC st
( [x,y] = [x1,y1] & S₁[x1,y1] ) ;
hence S₁[x,y] ; :: thesis:

end;

assume A40: S₁[x,y] ; :: thesis:
then consider s1 being Element of S such that
A41: s1 in C and
A42: [x,y] in E . s1 ;
A43: y in the Sorts of A . s1 by A42, ZFMISC_1:87;
( the Sorts of A . s1 in { ( the Sorts of A . s) where s is Element of S : s in C } & x in the Sorts of A . s1 ) by A41, A42, ZFMISC_1:87;
then reconsider x1 = x, y1 = y as Element of SAC by A43, TARSKI:def 4;
[x1,y1] in { [x,y] where x, y is Element of SAC : S₁[x,y] } by A40;
hence [x,y] in { [x,y] where x, y is Element of SAC : S₁[x,y] } ; :: thesis:

end;

hence for x, y being object holds
( [x,y] in P1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ; :: thesis:

end;