theorem Th7: :: BOR_CANT:7

for Omega being non empty set
for Sigma being SigmaField of Omega
for A being SetSequence of Sigma
for n being Nat holds (Partial_Intersection (Complement A)) . n = ((Partial_Union A) . n) `