theorem Th4: :: PARTIT1:4
for Y being non empty set
for PA, PB being a_partition of Y st PA '>' PB & PB '>' PA holds
PA = PB