for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n being Nat holds Prob . ((inferior_setsequence (Complement A)) . n) = 1 - (Prob . ((superior_setsequence A) . n))