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