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) `

let F be Subset-Family of X; :: thesis: Intersect (COMPLEMENT F) = (union F) `

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

end;

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;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

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;COMPLEMENT G = {} ;

hence Intersect (COMPLEMENT F) = (union F) ` by SETFAM_1:def 9, ZFMISC_1:2; :: thesis: verum