@John Baez [#15]: thanks.

> Definition. A partition P1 is finer than P2 if:
> P1and P2 partition the same set, and
> Every part of P1 is a subset of some part of P2.

Yes, that makes sense and is easier to read. I had an initial thought that subsets, in general, can be overlapping. Which would potentially require another clause. However, it's already implicit because P1 is a partition - and so already a disjoint union of subsets.