:: deftheorem Defdiff2 defines diff-c=-finite-partition-closed SRINGS_1:def 3 :
for X being set
for S being Subset-Family of X holds
( S is diff-c=-finite-partition-closed iff for S1, S2 being Element of S st S2 c= S1 holds
ex x being finite Subset of S st x is a_partition of S1 \ S2 );