for X being set
for S being cap-finite-partition-closed Subset-Family of X
for A being Element of S holds {{}} \/ (union ((PARTITIONS A) /\ (Fin S))) is semiring_of_sets of A