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:12; :: thesis: ( R is reflexive & R is symmetric & R is transitive & field R = X implies R is Equivalence_Relation of X )
assume that
A1: R is reflexive and
A2: ( R is symmetric & R is transitive ) and
A3: field R = X ; :: thesis: R is Equivalence_Relation of X
R is_reflexive_in X by A1, A3, RELAT_2:def 9;
then dom R = X by ORDERS_1:13;
hence R is Equivalence_Relation of X by A2, PARTFUN1:def 2; :: thesis: verum