let X be set ; :: thesis: for B being SetSequence of X holds lim_sup B = (lim_inf (Complement B)) `
let B be SetSequence of X; :: thesis: lim_sup B = (lim_inf (Complement B)) `
lim_inf (Complement B) = (lim_sup (Complement (Complement B))) ` by KURATO_2:12
.= (lim_sup B) ` ;
hence lim_sup B = (lim_inf (Complement B)) ` ; :: thesis: verum