for Omega being set
for ASeq being SetSequence of Omega
for Sigma being SigmaField of Omega st ASeq is SetSequence of Sigma holds
Union ASeq is Event of Sigma by Th17;