let R1, R2 be Equivalence_Relation of X; :: thesis: ( ( for x, y being object holds
( [x,y] in R1 iff ( x in X & y in X & f . x = f . y ) ) ) & ( for x, y being object holds
( [x,y] in R2 iff ( x in X & y in X & f . x = f . y ) ) ) implies R1 = R2 )
defpred S₁[ object , object ] means ( $1 in X & $2 in X & f . $1 = f . $2 );
assume for x, y being object holds
( [x,y] in R1 iff ( x in X & y in X & f . x = f . y ) ) ; :: thesis: ( ex x, y being object st
( ( [x,y] in R2 implies ( x in X & y in X & f . x = f . y ) ) implies ( x in X & y in X & f . x = f . y & not [x,y] in R2 ) ) or R1 = R2 )
then A4: for x, y being object holds
( [x,y] in R1 iff S₁[x,y] ) ;
assume for x, y being object holds
( [x,y] in R2 iff ( x in X & y in X & f . x = f . y ) ) ; :: thesis: R1 = R2
then A5: for x, y being object holds
( [x,y] in R2 iff S₁[x,y] ) ;
thus R1 = R2 from RELAT_1:sch 2(A4, A5); :: thesis: verum