let X be set ; :: thesis: 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 ) )
let R be Relation of X; :: thesis: ( R is Equivalence_Relation of X iff ( R is reflexive & R is symmetric & R is transitive & field R = X ) )
thus ( R is Equivalence_Relation of X implies ( R is reflexive & R is symmetric & R is transitive & field R = X ) ) by ORDERS_1:97; :: thesis: ( R is reflexive & R is symmetric & R is transitive & field R = X implies R is Equivalence_Relation of X )
assume A1: ( R is reflexive & R is symmetric & R is transitive & field R = X ) ; :: thesis: R is Equivalence_Relation of X
then R is_reflexive_in X by RELAT_2:def 9;
then dom R = X by ORDERS_1:98;
hence R is Equivalence_Relation of X by A1, PARTFUN1:def 4; :: thesis: verum