defpred S₁[ set , set ] means ex s1 being Element of S st
( s1 in C & [$1,$2] in E . s1 );
let X, Y be Equivalence_Relation of (the Sorts of A -carrier_of C); :: thesis: ( ( for x, y being set 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 set holds
( [x,y] in Y iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) ) ) implies X = Y )
assume A36: for x, y being set holds
( [x,y] in X iff S₁[x,y] ) ; :: thesis: ( ex x, y being set 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 A37: for x, y being set holds
( [x,y] in Y iff S₁[x,y] ) ; :: thesis: X = Y
for x, y being set holds
( [x,y] in X iff [x,y] in Y )

proof

let x, y be set ; :: 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 A36;
hence [x,y] in Y by A37; :: thesis: verum

end;

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

end;

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