for X being set
for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X
for A being Element of S
for Q being finite Subset of S st union Q c= A & Q is a_partition of union Q holds
ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )