theorem :: EQREL_1:35

for X being set
for y being object
for EqR being Equivalence_Relation of X
for x being object st x in X holds
( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) ) by Lm2;