theorem Th56: :: EC_PF_1:56

for X being non empty set
for R being Equivalence_Relation of X
for S being Class b₂ -valued Function st S is onto holds
Union S = X