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

let x, y be set ; :: 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 Th11; :: thesis: verum

end;

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