let X, Y be Equivalence_Relation of ( the Sorts of A -carrier_of C); :: thesis: ( ( for x, y being object holds
( [x,y] in X iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ) & ( for x, y being object holds
( [x,y] in Y iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ) implies X = Y )
defpred S₁[ object , object ] means ex s1 being Element of S st
( s1 in C & [$1,$2] in E . s1 );
assume A44: for x, y being object holds
( [x,y] in X iff S₁[x,y] ) ; :: thesis: ( ex x, y being object st
( ( [x,y] in Y implies ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) implies ( ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) & not [x,y] in Y ) ) or X = Y )
assume A45: for x, y being object holds
( [x,y] in Y iff S₁[x,y] ) ; :: thesis: X = Y
for x, y being object holds
( [x,y] in X iff [x,y] in Y )

proof

let x, y be object ; :: thesis: ( [x,y] in X iff [x,y] in Y )

hereby :: thesis: ( [x,y] in Y implies [x,y] in X )

assume [x,y] in X ; :: thesis: [x,y] in Y
then S₁[x,y] by A44;
hence [x,y] in Y by A45; :: thesis: verum

end;

assume [x,y] in Y ; :: thesis: [x,y] in X
then S₁[x,y] by A45;
hence [x,y] in X by A44; :: thesis: verum

end;

hence X = Y by RELAT_1:def 2; :: thesis: verum