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₁[ 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₁[x,y] ) by A18;
A21: for x, y being Element of A holds
( [x,y] in eq2 iff S₁[x,y] ) by A19;
thus eq1 = eq2 from RELSET_1:sch 4(A20, A21); :: thesis: verum