theorem Th10: :: SETLIM_1:10

for X being set
for A being Subset of X
for B being SetSequence of X st ( for n being Nat holds B . n = A ) holds
Union B = A