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 5
.= Union B ;
hence Union B = (Intersection (Complement B)) ` ; :: thesis: verum