let X be set ; :: thesis: for Si being SigmaField of X

for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) `

let Si be SigmaField of X; :: thesis: for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) `

let S be SetSequence of Si; :: thesis: lim_inf S = (lim_sup (Complement S)) `

for B being SetSequence of X holds Union (inferior_setsequence B) = (Intersection (superior_setsequence (Complement B))) `

for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) `

let Si be SigmaField of X; :: thesis: for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) `

let S be SetSequence of Si; :: thesis: lim_inf S = (lim_sup (Complement S)) `

for B being SetSequence of X holds Union (inferior_setsequence B) = (Intersection (superior_setsequence (Complement B))) `

proof

hence
lim_inf S = (lim_sup (Complement S)) `
; :: thesis: verum
let B be SetSequence of X; :: thesis: Union (inferior_setsequence B) = (Intersection (superior_setsequence (Complement B))) `

( lim_inf B = Union (inferior_setsequence B) & (lim_sup (Complement B)) ` = (Intersection (superior_setsequence (Complement B))) ` ) ;

hence Union (inferior_setsequence B) = (Intersection (superior_setsequence (Complement B))) ` by KURATO_0:9; :: thesis: verum

end;( lim_inf B = Union (inferior_setsequence B) & (lim_sup (Complement B)) ` = (Intersection (superior_setsequence (Complement B))) ` ) ;

hence Union (inferior_setsequence B) = (Intersection (superior_setsequence (Complement B))) ` by KURATO_0:9; :: thesis: verum