theorem :: PROB_3:32

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_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds
not x in XSeq . k ) ) )