theorem Th5: :: PARTIT1:5

for Y being non empty set
for PA, PB being a_partition of Y st PA '>' PB holds
PA is_coarser_than PB