theorem :: EQREL_1:3

for X being set holds id X is Equivalence_Relation of X ;