let X be 1-sorted ; :: thesis: for F being Subset-Family of X holds Intersect (COMPLEMENT F) = (union F) `
let F be Subset-Family of X; :: 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:32;
hence Intersect (COMPLEMENT F) = meet (COMPLEMENT F) by SETFAM_1:def 9
.= ([#] the carrier of X) \ (union F) by A1, SETFAM_1:33
.= (union F) ` ;
:: thesis: verum
end;
suppose F = {} ; :: thesis: Intersect (COMPLEMENT F) = (union F) `
then reconsider G = F as empty Subset-Family of X ;
COMPLEMENT G = {} ;
hence Intersect (COMPLEMENT F) = (union F) ` by SETFAM_1:def 9, ZFMISC_1:2; :: thesis: verum
end;
end;