theorem Th25: :: PARTIT1:25

for Y being non empty set
for PA, PB being a_partition of Y st ERl PA = ERl PB holds
PA = PB