theorem Thm1: :: SRINGS_1:8

for X being set
for S being diff-finite-partition-closed Subset-Family of X
for S1 being Element of S
for T being finite Subset of S ex P being finite Subset of S st P is a_partition of S1 \ (union T)