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 R = Y by ORDERS_1:97;
A3: field S = Y by ORDERS_1:97;
then ( R is_reflexive_in Y & S is_reflexive_in Y ) by A2, RELAT_2:def 9;
then R * S is_reflexive_in Y by Th7;
then A4: ( field (R * S) = Y & dom (R * S) = Y ) by ORDERS_1:98;
( R * S is total & R * S is symmetric & R * S is transitive )

proof

thus R * S is total by A4, PARTFUN1:def 4; :: thesis: ( R * S is symmetric & R * S is transitive )
R * S is_symmetric_in Y

proof

A5: R is_symmetric_in Y by A2, RELAT_2:def 11;
A6: S is_symmetric_in Y by A3, RELAT_2:def 11;
let x, y be set ; :: 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
A7: x in Y and
A8: 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 set such that
A9: [x,z] in R and
A10: [z,y] in S by RELAT_1:def 8;
z in field R by A9, RELAT_1:30;
then A11: [z,x] in R by A2, A5, A7, A9, RELAT_2:def 3;
z in field S by A10, RELAT_1:30;
then [y,z] in S by A3, A6, A8, A10, RELAT_2:def 3;
hence [y,x] in R * S by A1, A11, RELAT_1:def 8; :: thesis: verum

end;

hence R * S is symmetric by A4, RELAT_2:def 11; :: thesis: R * S is transitive
A12: R * R c= R by RELAT_2:44;
A13: S * S c= S by RELAT_2:44;
(R * S) * (R * S) = ((R * S) * R) * S by RELAT_1:55
.= (R * (R * S)) * S by A1, RELAT_1:55
.= ((R * R) * S) * S by RELAT_1:55
.= (R * R) * (S * S) by RELAT_1:55 ;
then (R * S) * (R * S) c= R * S by A12, A13, RELAT_1:50;
hence R * S is transitive by RELAT_2:44; :: thesis: verum

end;

hence R * S is Equivalence_Relation of Y ; :: thesis: verum