let X be set ; :: thesis: for Si being SigmaField of X
for S being SetSequence of holds lim_sup S = (lim_inf (@Complement S)) `
let Si be SigmaField of X; :: thesis: for S being SetSequence of holds lim_sup S = (lim_inf (@Complement S)) `
let S be SetSequence of ; :: thesis: lim_sup S = (lim_inf (@Complement S)) `
lim_inf (@Complement S) = (lim_sup (@Complement (@Complement S))) ` by Th205
.= (lim_sup S) ` ;
hence lim_sup S = (lim_inf (@Complement S)) ` ; :: thesis: verum