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