for X being set
for S being cap-finite-partition-closed Subset-Family of X
for A being Element of S holds { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } is diff-c=-finite-partition-closed Subset-Family of A