for X being set
for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X
for SM being finite Subset of S ex P being finite Subset of S st
( P is a_partition of union SM & ( for Y being Element of SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } ) )