let X be 1-sorted ; :: thesis: for F being Subset-Family of X holds union (COMPLEMENT F) = (Intersect F) `
let F be Subset-Family of X; :: thesis: union (COMPLEMENT F) = (Intersect F) `
thus union (COMPLEMENT F) = ((union (COMPLEMENT F)) `) `
.= (Intersect (COMPLEMENT (COMPLEMENT F))) ` by Th6
.= (Intersect F) ` ; :: thesis: verum