theorem :: PROB_3:26

for n being Nat
for x being object
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (Partial_Union XSeq) . n iff ex k being Nat st
( k <= n & x in XSeq . k ) )