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

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