theorem :: FINSEQ_4:86

for Y being set
for E1, E2 being Equivalence_Relation of Y st Class E1 = Class E2 holds
E1 = E2