for X being set
for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X holds S is diff-finite-partition-closed