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))) `
proof
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;
hence lim_inf S = (lim_sup (Complement S)) ` ; :: thesis: verum