let eq1, eq2 be Equivalence_Relation of the carrier of A; :: thesis: ( ( for x, y being Element of A holds

( [x,y] in eq1 iff ( x <= y & y <= x ) ) ) & ( for x, y being Element of A holds

( [x,y] in eq2 iff ( x <= y & y <= x ) ) ) implies eq1 = eq2 )

assume that

A18: for x, y being Element of A holds

( [x,y] in eq1 iff ( x <= y & y <= x ) ) and

A19: for x, y being Element of A holds

( [x,y] in eq2 iff ( x <= y & y <= x ) ) ; :: thesis: eq1 = eq2

defpred S_{1}[ Element of A, Element of A] means ( $1 <= $2 & $2 <= $1 );

A20: for x, y being Element of A holds

( [x,y] in eq1 iff S_{1}[x,y] )
by A18;

A21: for x, y being Element of A holds

( [x,y] in eq2 iff S_{1}[x,y] )
by A19;

thus eq1 = eq2 from RELSET_1:sch 4(A20, A21); :: thesis: verum

( [x,y] in eq1 iff ( x <= y & y <= x ) ) ) & ( for x, y being Element of A holds

( [x,y] in eq2 iff ( x <= y & y <= x ) ) ) implies eq1 = eq2 )

assume that

A18: for x, y being Element of A holds

( [x,y] in eq1 iff ( x <= y & y <= x ) ) and

A19: for x, y being Element of A holds

( [x,y] in eq2 iff ( x <= y & y <= x ) ) ; :: thesis: eq1 = eq2

defpred S

A20: for x, y being Element of A holds

( [x,y] in eq1 iff S

A21: for x, y being Element of A holds

( [x,y] in eq2 iff S

thus eq1 = eq2 from RELSET_1:sch 4(A20, A21); :: thesis: verum