for X being set
for S being cap-finite-partition-closed Subset-Family of X
for A being Element of S holds
( union ((PARTITIONS A) /\ (Fin S)) is cap-finite-partition-closed diff-finite-partition-closed Subset-Family of A & union ((PARTITIONS A) /\ (Fin S)) is with_non-empty_elements )