theorem Thm4: :: SRINGS_1:15

for X being set
for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X
for SM being Function of NATPLUS,S ex P being countable Subset of S st
( P is a_partition of Union SM & ( for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in P & s c= Union (SM | (Seg n)) ) } ) )