let X be set ; :: thesis: for EqR being Equivalence_Relation of X holds (id X) /\ EqR = id X
let EqR be Equivalence_Relation of X; :: thesis: (id X) /\ EqR = id X

now :: thesis: for x, y being object st [x,y] in id X holds
[x,y] in EqR

let x, y be object ; :: thesis: ( [x,y] in id X implies [x,y] in EqR )
assume [x,y] in id X ; :: thesis: [x,y] in EqR
then ( x in X & x = y ) by RELAT_1:def 10;
hence [x,y] in EqR by Th5; :: thesis: verum

end;

then id X c= EqR ;
hence (id X) /\ EqR = id X by XBOOLE_1:28; :: thesis: verum