let X be set ; :: thesis: nabla X is Equivalence_Relation of X

for x, y being object st x in X & y in X & [x,y] in nabla X holds

[y,x] in nabla X by ZFMISC_1:88;

then A1: nabla X is_symmetric_in X ;

for x, y, z being object st x in X & y in X & z in X & [x,y] in nabla X & [y,z] in nabla X holds

[x,z] in nabla X by ZFMISC_1:87;

then A2: nabla X is_transitive_in X ;

field (nabla X) = X by ORDERS_1:12;

hence nabla X is Equivalence_Relation of X by A1, A2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum

for x, y being object st x in X & y in X & [x,y] in nabla X holds

[y,x] in nabla X by ZFMISC_1:88;

then A1: nabla X is_symmetric_in X ;

for x, y, z being object st x in X & y in X & z in X & [x,y] in nabla X & [y,z] in nabla X holds

[x,z] in nabla X by ZFMISC_1:87;

then A2: nabla X is_transitive_in X ;

field (nabla X) = X by ORDERS_1:12;

hence nabla X is Equivalence_Relation of X by A1, A2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum