theorem Th9: :: EQREL_1:9

for X being set
for R being Relation of X holds
( R is Equivalence_Relation of X iff ( R is reflexive & R is symmetric & R is transitive & field R = X ) ) by ORDERS_1:12, ORDERS_1:13, PARTFUN1:def 2;