theorem thmCup: :: SRINGS_1:21

for X being set
for S being cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is cup-closed