for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma st ASeq is V77() holds
for n, m being Nat st n < m holds
(Partial_Union ASeq) . n misses ASeq . m