theorem Thm2: :: SRINGS_1:9

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