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