theorem ThmVAL1: :: SRINGS_1:2

for X being set
for S being Subset-Family of X
for A being Element of S holds { x where x is Element of S : x in union ((PARTITIONS A) /\ (Fin S)) } = union ((PARTITIONS A) /\ (Fin S))