let R, S be Equivalence_Relation of ( the Sorts of U1 . s); :: thesis: ( ( for x, y being Element of the Sorts of U1 . s holds
( [x,y] in R iff (F . s) . x = (F . s) . y ) ) & ( for x, y being Element of the Sorts of U1 . s holds
( [x,y] in S iff (F . s) . x = (F . s) . y ) ) implies R = S )
assume that
A5: for x, y being Element of the Sorts of U1 . s holds
( [x,y] in R iff (F . s) . x = (F . s) . y ) and
A6: for x, y being Element of the Sorts of U1 . s holds
( [x,y] in S iff (F . s) . x = (F . s) . y ) ; :: thesis: R = S
now :: thesis: for x, y being object holds
( ( [x,y] in R implies [x,y] in S ) & ( [x,y] in S implies [x,y] in R ) )
let x, y be object ; :: thesis: ( ( [x,y] in R implies [x,y] in S ) & ( [x,y] in S implies [x,y] in R ) )
thus ( [x,y] in R implies [x,y] in S ) :: thesis: ( [x,y] in S implies [x,y] in R )
proof
assume A7: [x,y] in R ; :: thesis: [x,y] in S
then reconsider a = x, b = y as Element of the Sorts of U1 . s by ZFMISC_1:87;
(F . s) . a = (F . s) . b by A5, A7;
hence [x,y] in S by A6; :: thesis: verum
end;
assume A8: [x,y] in S ; :: thesis: [x,y] in R
then reconsider a = x, b = y as Element of the Sorts of U1 . s by ZFMISC_1:87;
(F . s) . a = (F . s) . b by A6, A8;
hence [x,y] in R by A5; :: thesis: verum
end;
hence R = S by RELAT_1:def 2; :: thesis: verum