theorem Th55: :: EC_PF_1:55

for X being non empty set
for R being Equivalence_Relation of X
for S being Class b₂ -valued Function st S is one-to-one holds
S is disjoint_valued