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

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

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

then
id X c= EqR
;[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;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

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