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