theorem :: PROB_3:34

for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds (Partial_Diff_Union XSeq) . n c= (Partial_Union XSeq) . n by Th18;