let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A being SetSequence of Sigma
for n being Nat holds (inferior_setsequence (Complement A)) . n = ((superior_setsequence A) . n) `
let Sigma be SigmaField of Omega; :: thesis: for A being SetSequence of Sigma
for n being Nat holds (inferior_setsequence (Complement A)) . n = ((superior_setsequence A) . n) `
let A be SetSequence of Sigma; :: thesis: for n being Nat holds (inferior_setsequence (Complement A)) . n = ((superior_setsequence A) . n) `
let n be Nat; :: thesis: (inferior_setsequence (Complement A)) . n = ((superior_setsequence A) . n) `
set B = Complement A;
n in NAT by ORDINAL1:def 12;
then (inferior_setsequence (Complement A)) . n = ((superior_setsequence (Complement (Complement A))) . n) ` by SETLIM_1:30;
hence (inferior_setsequence (Complement A)) . n = ((superior_setsequence A) . n) ` ; :: thesis: verum