for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si st XSeq is non-descending holds
Partial_Union XSeq = XSeq by Th15;