let T be set ; :: thesis: for F being Subset-Family of T st F <> {} holds
union (COMPLEMENT F) = (meet F) `
let F be Subset-Family of T; :: thesis: ( F <> {} implies union (COMPLEMENT F) = (meet F) ` )
assume F <> {} ; :: thesis: union (COMPLEMENT F) = (meet F) `
then union (COMPLEMENT F) = ([#] T) \ (meet F) by SETFAM_1:34
.= T \ (meet F) ;
hence union (COMPLEMENT F) = (meet F) ` ; :: thesis: verum