for X being set
for D being a_partition of X
for P1, P2 being Subset of D st union P1 = union P2 holds
P1 = P2 by Th1;