theorem :: PROB_4:20

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si st XSeq is non-descending holds
( (Partial_Diff_Union XSeq) . 0 = XSeq . 0 & ( for n being Element of NAT holds (Partial_Diff_Union XSeq) . (n + 1) = (XSeq . (n + 1)) \ (XSeq . n) ) ) by Th16;