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