for X being set
for S being cap-finite-partition-closed Subset-Family of X
for A, B being finite Subset of S st A is mutually-disjoint & B is mutually-disjoint holds
ex P being finite Subset of S st P is a_partition of (union A) /\ (union B)