for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Union (Partial_Diff_Union XSeq) = Union XSeq by Th20;