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