let X be set ; :: thesis: for B being SetSequence of X holds Union B = (Intersection (Complement B)) `
let B be SetSequence of X; :: thesis: Union B = (Intersection (Complement B)) `
(Intersection (Complement B)) ` = ((Union (Complement (Complement B))) `) ` by PROB_1:def 3
.= Union B ;
hence Union B = (Intersection (Complement B)) ` ; :: thesis: verum