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

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