theorem Th34: :: EQREL_1:34

for X being set
for P being a_partition of X ex EqR being Equivalence_Relation of X st P = Class EqR