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

per cases ( F <> {} or F = {} ) ;

suppose A1: F <> {} ; :: thesis: Intersect (COMPLEMENT F) = (union F) `

then COMPLEMENT F <> {} by SETFAM_1:46;
hence Intersect (COMPLEMENT F) = meet (COMPLEMENT F) by SETFAM_1:def 10
.= ([#] the carrier of X) \ (union F) by A1, SETFAM_1:47
.= (union F) ` ;
:: thesis: verum

end;

suppose F = {} ; :: thesis: Intersect (COMPLEMENT F) = (union F) `

then reconsider G = F as empty Subset-Family of ;
COMPLEMENT G = {} ;
hence Intersect (COMPLEMENT F) = (union F) ` by SETFAM_1:def 10, ZFMISC_1:2; :: thesis: verum

end;

end;