theorem Th32: :: PARTIT1:32

for Y being non empty set
for PA being a_partition of Y holds
( %O Y '>' PA & PA '>' %I Y )