let Y be non empty set ; :: thesis: for R, S being Equivalence_Relation of Y st R * S = S * R holds
R * S is Equivalence_Relation of Y
let R, S be Equivalence_Relation of Y; :: thesis: ( R * S = S * R implies R * S is Equivalence_Relation of Y )
assume A1: R * S = S * R ; :: thesis: R * S is Equivalence_Relation of Y
A2: field S = Y by ORDERS_1:12;
then A3: S is_reflexive_in Y by RELAT_2:def 9;
A4: field R = Y by ORDERS_1:12;
then R is_reflexive_in Y by RELAT_2:def 9;
then R * S is_reflexive_in Y by A3, Th7;
then A5: ( field (R * S) = Y & dom (R * S) = Y ) by ORDERS_1:13;
A6: R * S is_symmetric_in Y

proof

A7: S is_symmetric_in Y by A2, RELAT_2:def 11;
let x, y be object ; :: according to RELAT_2:def 3 :: thesis: ( not x in Y or not y in Y or not [x,y] in R * S or [y,x] in R * S )
assume that
A8: x in Y and
A9: y in Y ; :: thesis: ( not [x,y] in R * S or [y,x] in R * S )
assume [x,y] in R * S ; :: thesis: [y,x] in R * S
then consider z being object such that
A10: [x,z] in R and
A11: [z,y] in S by RELAT_1:def 8;
z in field S by A11, RELAT_1:15;
then A12: [y,z] in S by A2, A7, A9, A11;
A13: R is_symmetric_in Y by A4, RELAT_2:def 11;
z in field R by A10, RELAT_1:15;
then [z,x] in R by A4, A13, A8, A10;
hence [y,x] in R * S by A1, A12, RELAT_1:def 8; :: thesis: verum

end;

A14: ( R * R c= R & S * S c= S ) by RELAT_2:27;
(R * S) * (R * S) = ((R * S) * R) * S by RELAT_1:36
.= (R * (R * S)) * S by A1, RELAT_1:36
.= ((R * R) * S) * S by RELAT_1:36
.= (R * R) * (S * S) by RELAT_1:36 ;
then (R * S) * (R * S) c= R * S by A14, RELAT_1:31;
hence R * S is Equivalence_Relation of Y by A5, A6, PARTFUN1:def 2, RELAT_2:27, RELAT_2:def 11; :: thesis: verum