theorem :: EQREL_1:10

for X being set
for EqR being Equivalence_Relation of X holds (id X) /\ EqR = id X