let X, Y be Equivalence_Relation of ( the Sorts of A -carrier_of C); ( ( 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 S1[ 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 S1[x,y] )
; ( 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 S1[x,y] )
; X = Y
for x, y being object holds
( [x,y] in X iff [x,y] in Y )
hence
X = Y
by RELAT_1:def 2; verum