theorem :: PROB_3:22

for X being set
for Si being SigmaField of X
for XSeq, YSeq being SetSequence of Si st YSeq = Partial_Union XSeq holds
( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (YSeq . n) \/ (XSeq . (n + 1)) ) ) by Def2;